Proof of Theorem nvof1o
Step | Hyp | Ref
| Expression |
1 | | fnfun 5902 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
2 | | fdmrn 5977 |
. . . . . 6
⊢ (Fun
𝐹 ↔ 𝐹:dom 𝐹⟶ran 𝐹) |
3 | 1, 2 | sylib 207 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → 𝐹:dom 𝐹⟶ran 𝐹) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:dom 𝐹⟶ran 𝐹) |
5 | | fndm 5904 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → dom 𝐹 = 𝐴) |
7 | | df-rn 5049 |
. . . . . . 7
⊢ ran 𝐹 = dom ◡𝐹 |
8 | | dmeq 5246 |
. . . . . . 7
⊢ (◡𝐹 = 𝐹 → dom ◡𝐹 = dom 𝐹) |
9 | 7, 8 | syl5eq 2656 |
. . . . . 6
⊢ (◡𝐹 = 𝐹 → ran 𝐹 = dom 𝐹) |
10 | 9, 5 | sylan9eqr 2666 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → ran 𝐹 = 𝐴) |
11 | 6, 10 | feq23d 5953 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → (𝐹:dom 𝐹⟶ran 𝐹 ↔ 𝐹:𝐴⟶𝐴)) |
12 | 4, 11 | mpbid 221 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴⟶𝐴) |
13 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → Fun 𝐹) |
14 | | funeq 5823 |
. . . . 5
⊢ (◡𝐹 = 𝐹 → (Fun ◡𝐹 ↔ Fun 𝐹)) |
15 | 14 | adantl 481 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → (Fun ◡𝐹 ↔ Fun 𝐹)) |
16 | 13, 15 | mpbird 246 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → Fun ◡𝐹) |
17 | | df-f1 5809 |
. . 3
⊢ (𝐹:𝐴–1-1→𝐴 ↔ (𝐹:𝐴⟶𝐴 ∧ Fun ◡𝐹)) |
18 | 12, 16, 17 | sylanbrc 695 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1→𝐴) |
19 | | simpl 472 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹 Fn 𝐴) |
20 | | df-fo 5810 |
. . 3
⊢ (𝐹:𝐴–onto→𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴)) |
21 | 19, 10, 20 | sylanbrc 695 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–onto→𝐴) |
22 | | df-f1o 5811 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐴 ↔ (𝐹:𝐴–1-1→𝐴 ∧ 𝐹:𝐴–onto→𝐴)) |
23 | 18, 21, 22 | sylanbrc 695 |
1
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴) |