Proof of Theorem nvof1o
| Step | Hyp | Ref
| Expression |
| 1 | | fnfun 6668 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
| 2 | | fdmrn 6767 |
. . . . . 6
⊢ (Fun
𝐹 ↔ 𝐹:dom 𝐹⟶ran 𝐹) |
| 3 | 1, 2 | sylib 218 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → 𝐹:dom 𝐹⟶ran 𝐹) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:dom 𝐹⟶ran 𝐹) |
| 5 | | fndm 6671 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → dom 𝐹 = 𝐴) |
| 7 | | df-rn 5696 |
. . . . . . 7
⊢ ran 𝐹 = dom ◡𝐹 |
| 8 | | dmeq 5914 |
. . . . . . 7
⊢ (◡𝐹 = 𝐹 → dom ◡𝐹 = dom 𝐹) |
| 9 | 7, 8 | eqtrid 2789 |
. . . . . 6
⊢ (◡𝐹 = 𝐹 → ran 𝐹 = dom 𝐹) |
| 10 | 9, 5 | sylan9eqr 2799 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → ran 𝐹 = 𝐴) |
| 11 | 6, 10 | feq23d 6731 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → (𝐹:dom 𝐹⟶ran 𝐹 ↔ 𝐹:𝐴⟶𝐴)) |
| 12 | 4, 11 | mpbid 232 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴⟶𝐴) |
| 13 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → Fun 𝐹) |
| 14 | | funeq 6586 |
. . . . 5
⊢ (◡𝐹 = 𝐹 → (Fun ◡𝐹 ↔ Fun 𝐹)) |
| 15 | 14 | adantl 481 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → (Fun ◡𝐹 ↔ Fun 𝐹)) |
| 16 | 13, 15 | mpbird 257 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → Fun ◡𝐹) |
| 17 | | df-f1 6566 |
. . 3
⊢ (𝐹:𝐴–1-1→𝐴 ↔ (𝐹:𝐴⟶𝐴 ∧ Fun ◡𝐹)) |
| 18 | 12, 16, 17 | sylanbrc 583 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1→𝐴) |
| 19 | | simpl 482 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹 Fn 𝐴) |
| 20 | | df-fo 6567 |
. . 3
⊢ (𝐹:𝐴–onto→𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴)) |
| 21 | 19, 10, 20 | sylanbrc 583 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–onto→𝐴) |
| 22 | | df-f1o 6568 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐴 ↔ (𝐹:𝐴–1-1→𝐴 ∧ 𝐹:𝐴–onto→𝐴)) |
| 23 | 18, 21, 22 | sylanbrc 583 |
1
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴) |