Proof of Theorem dff1o2
Step | Hyp | Ref
| Expression |
1 | | df-f1o 4852 |
. 2
⊢ (𝐹:A–1-1-onto→B ↔
(𝐹:A–1-1→B ∧ 𝐹:A–onto→B)) |
2 | | df-f1 4850 |
. . . 4
⊢ (𝐹:A–1-1→B ↔
(𝐹:A⟶B ∧ Fun ◡𝐹)) |
3 | | df-fo 4851 |
. . . 4
⊢ (𝐹:A–onto→B ↔
(𝐹 Fn A ∧ ran 𝐹 = B)) |
4 | 2, 3 | anbi12i 433 |
. . 3
⊢ ((𝐹:A–1-1→B ∧ 𝐹:A–onto→B) ↔
((𝐹:A⟶B ∧ Fun ◡𝐹) ∧ (𝐹 Fn A
∧ ran 𝐹 = B))) |
5 | | anass 381 |
. . . 4
⊢ (((𝐹:A⟶B ∧ Fun ◡𝐹) ∧ (𝐹 Fn A
∧ ran 𝐹 = B))
↔ (𝐹:A⟶B ∧ (Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B)))) |
6 | | 3anan12 896 |
. . . . . 6
⊢ ((𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B) ↔ (Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B))) |
7 | 6 | anbi1i 431 |
. . . . 5
⊢ (((𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B) ∧ 𝐹:A⟶B)
↔ ((Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B)) ∧ 𝐹:A⟶B)) |
8 | | eqimss 2991 |
. . . . . . . 8
⊢ (ran
𝐹 = B → ran 𝐹 ⊆ B) |
9 | | df-f 4849 |
. . . . . . . . 9
⊢ (𝐹:A⟶B
↔ (𝐹 Fn A ∧ ran 𝐹 ⊆ B)) |
10 | 9 | biimpri 124 |
. . . . . . . 8
⊢ ((𝐹 Fn A ∧ ran 𝐹 ⊆ B) → 𝐹:A⟶B) |
11 | 8, 10 | sylan2 270 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ ran 𝐹 = B) → 𝐹:A⟶B) |
12 | 11 | 3adant2 922 |
. . . . . 6
⊢ ((𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B) → 𝐹:A⟶B) |
13 | 12 | pm4.71i 371 |
. . . . 5
⊢ ((𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B) ↔ ((𝐹 Fn A
∧ Fun ◡𝐹 ∧ ran
𝐹 = B) ∧ 𝐹:A⟶B)) |
14 | | ancom 253 |
. . . . 5
⊢ ((𝐹:A⟶B ∧ (Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B))) ↔ ((Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B)) ∧ 𝐹:A⟶B)) |
15 | 7, 13, 14 | 3bitr4ri 202 |
. . . 4
⊢ ((𝐹:A⟶B ∧ (Fun ◡𝐹 ∧ (𝐹 Fn A ∧ ran 𝐹 = B))) ↔ (𝐹 Fn A
∧ Fun ◡𝐹 ∧ ran
𝐹 = B)) |
16 | 5, 15 | bitri 173 |
. . 3
⊢ (((𝐹:A⟶B ∧ Fun ◡𝐹) ∧ (𝐹 Fn A
∧ ran 𝐹 = B))
↔ (𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B)) |
17 | 4, 16 | bitri 173 |
. 2
⊢ ((𝐹:A–1-1→B ∧ 𝐹:A–onto→B) ↔
(𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B)) |
18 | 1, 17 | bitri 173 |
1
⊢ (𝐹:A–1-1-onto→B ↔
(𝐹 Fn A ∧ Fun ◡𝐹 ∧ ran
𝐹 = B)) |