Proof of Theorem f1finf1o
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . 4
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1→𝐵) |
2 | | f1f 6721 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
3 | 2 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴⟶𝐵) |
4 | 3 | ffnd 6652 |
. . . . 5
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴) |
5 | | simpll 764 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ 𝐵) |
6 | 3 | frnd 6659 |
. . . . . . . . 9
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 ⊆ 𝐵) |
7 | | df-pss 3917 |
. . . . . . . . . 10
⊢ (ran
𝐹 ⊊ 𝐵 ↔ (ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ 𝐵)) |
8 | 7 | baib 536 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ 𝐵 → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵)) |
9 | 6, 8 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵)) |
10 | | php3 9077 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ ran 𝐹 ⊊ 𝐵) → ran 𝐹 ≺ 𝐵) |
11 | 10 | ex 413 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵)) |
12 | 11 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵)) |
13 | | enfii 9054 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) |
14 | 13 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
15 | | f1f1orn 6778 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
16 | | f1oenfi 9047 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→ran
𝐹) → 𝐴 ≈ ran 𝐹) |
17 | 14, 15, 16 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ ran 𝐹) |
18 | | endom 8840 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≈ ran 𝐹 → 𝐴 ≼ ran 𝐹) |
19 | | domsdomtrfi 9070 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵) → 𝐴 ≺ 𝐵) |
20 | 18, 19 | syl3an2 1163 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵) → 𝐴 ≺ 𝐵) |
21 | 20 | 3expia 1120 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ ran 𝐹) → (ran 𝐹 ≺ 𝐵 → 𝐴 ≺ 𝐵)) |
22 | 14, 17, 21 | syl2an2r 682 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ≺ 𝐵 → 𝐴 ≺ 𝐵)) |
23 | 12, 22 | syld 47 |
. . . . . . . . 9
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → 𝐴 ≺ 𝐵)) |
24 | | sdomnen 8842 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
25 | 23, 24 | syl6 35 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
26 | 9, 25 | sylbird 259 |
. . . . . . 7
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ≠ 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
27 | 26 | necon4ad 2959 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (𝐴 ≈ 𝐵 → ran 𝐹 = 𝐵)) |
28 | 5, 27 | mpd 15 |
. . . . 5
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 = 𝐵) |
29 | | df-fo 6485 |
. . . . 5
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
30 | 4, 28, 29 | sylanbrc 583 |
. . . 4
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–onto→𝐵) |
31 | | df-f1o 6486 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
32 | 1, 30, 31 | sylanbrc 583 |
. . 3
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1-onto→𝐵) |
33 | 32 | ex 413 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→𝐵)) |
34 | | f1of1 6766 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
35 | 33, 34 | impbid1 224 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) |