Step | Hyp | Ref
| Expression |
1 | | bren 8896 |
. 2
⊢ (suc
𝐴 ≈ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴–1-1-onto→suc
𝐵) |
2 | | f1of1 6784 |
. . . . . . . . 9
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → 𝑓:suc 𝐴–1-1→suc 𝐵) |
3 | | nnfi 9114 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
4 | | sssucid 6398 |
. . . . . . . . . 10
⊢ 𝐴 ⊆ suc 𝐴 |
5 | | f1imaenfi 9145 |
. . . . . . . . . 10
⊢ ((𝑓:suc 𝐴–1-1→suc 𝐵 ∧ 𝐴 ⊆ suc 𝐴 ∧ 𝐴 ∈ Fin) → (𝑓 “ 𝐴) ≈ 𝐴) |
6 | 4, 5 | mp3an2 1450 |
. . . . . . . . 9
⊢ ((𝑓:suc 𝐴–1-1→suc 𝐵 ∧ 𝐴 ∈ Fin) → (𝑓 “ 𝐴) ≈ 𝐴) |
7 | 2, 3, 6 | syl2anr 598 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → (𝑓 “ 𝐴) ≈ 𝐴) |
8 | | ensymfib 9134 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝐴 ≈ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐴) ≈ 𝐴)) |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 ≈ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐴) ≈ 𝐴)) |
10 | 9 | adantr 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → (𝐴 ≈ (𝑓 “ 𝐴) ↔ (𝑓 “ 𝐴) ≈ 𝐴)) |
11 | 7, 10 | mpbird 257 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → 𝐴 ≈ (𝑓 “ 𝐴)) |
12 | | nnord 7811 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → Ord 𝐴) |
13 | | orddif 6414 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 𝐴 = (suc 𝐴 ∖ {𝐴})) |
15 | 14 | imaeq2d 6014 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑓 “ 𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴}))) |
16 | | f1ofn 6786 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → 𝑓 Fn suc 𝐴) |
17 | | phplem2.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
18 | 17 | sucid 6400 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ suc 𝐴 |
19 | | fnsnfv 6921 |
. . . . . . . . . . 11
⊢ ((𝑓 Fn suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
20 | 16, 18, 19 | sylancl 587 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
21 | 20 | difeq2d 4083 |
. . . . . . . . 9
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → ((𝑓 “ suc 𝐴) ∖ {(𝑓‘𝐴)}) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
22 | | imadmrn 6024 |
. . . . . . . . . . . 12
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
23 | 22 | eqcomi 2742 |
. . . . . . . . . . 11
⊢ ran 𝑓 = (𝑓 “ dom 𝑓) |
24 | | f1ofo 6792 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → 𝑓:suc 𝐴–onto→suc 𝐵) |
25 | | forn 6760 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–onto→suc 𝐵 → ran 𝑓 = suc 𝐵) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → ran 𝑓 = suc 𝐵) |
27 | | f1odm 6789 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → dom 𝑓 = suc 𝐴) |
28 | 27 | imaeq2d 6014 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (𝑓 “ dom 𝑓) = (𝑓 “ suc 𝐴)) |
29 | 23, 26, 28 | 3eqtr3a 2797 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → suc 𝐵 = (𝑓 “ suc 𝐴)) |
30 | 29 | difeq1d 4082 |
. . . . . . . . 9
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (suc 𝐵 ∖ {(𝑓‘𝐴)}) = ((𝑓 “ suc 𝐴) ∖ {(𝑓‘𝐴)})) |
31 | | dff1o3 6791 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 ↔ (𝑓:suc 𝐴–onto→suc 𝐵 ∧ Fun ◡𝑓)) |
32 | | imadif 6586 |
. . . . . . . . . 10
⊢ (Fun
◡𝑓 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
33 | 31, 32 | simplbiim 506 |
. . . . . . . . 9
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
34 | 21, 30, 33 | 3eqtr4rd 2784 |
. . . . . . . 8
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
35 | 15, 34 | sylan9eq 2793 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → (𝑓 “ 𝐴) = (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
36 | 11, 35 | breqtrd 5132 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → 𝐴 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
37 | | fnfvelrn 7032 |
. . . . . . . . . . . 12
⊢ ((𝑓 Fn suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → (𝑓‘𝐴) ∈ ran 𝑓) |
38 | 16, 18, 37 | sylancl 587 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (𝑓‘𝐴) ∈ ran 𝑓) |
39 | 25 | eleq2d 2820 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–onto→suc 𝐵 → ((𝑓‘𝐴) ∈ ran 𝑓 ↔ (𝑓‘𝐴) ∈ suc 𝐵)) |
40 | 24, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → ((𝑓‘𝐴) ∈ ran 𝑓 ↔ (𝑓‘𝐴) ∈ suc 𝐵)) |
41 | 38, 40 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → (𝑓‘𝐴) ∈ suc 𝐵) |
42 | | phplem1 9154 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ω ∧ (𝑓‘𝐴) ∈ suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
43 | 41, 42 | sylan2 594 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
44 | | nnfi 9114 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ω → 𝐵 ∈ Fin) |
45 | | ensymfib 9134 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → (𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ↔ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → (𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ↔ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵)) |
47 | 46 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → (𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ↔ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵)) |
48 | 43, 47 | mpbid 231 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵) |
49 | | entrfil 9135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵) → 𝐴 ≈ 𝐵) |
50 | 3, 49 | syl3an1 1164 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵) → 𝐴 ≈ 𝐵) |
51 | 48, 50 | syl3an3 1166 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ∧ (𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵)) → 𝐴 ≈ 𝐵) |
52 | 51 | 3expa 1119 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐴 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) ∧ (𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵)) → 𝐴 ≈ 𝐵) |
53 | 36, 52 | syldanl 603 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) ∧ (𝐵 ∈ ω ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵)) → 𝐴 ≈ 𝐵) |
54 | 53 | anandirs 678 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑓:suc 𝐴–1-1-onto→suc
𝐵) → 𝐴 ≈ 𝐵) |
55 | 54 | ex 414 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝑓:suc 𝐴–1-1-onto→suc
𝐵 → 𝐴 ≈ 𝐵)) |
56 | 55 | exlimdv 1937 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑓 𝑓:suc 𝐴–1-1-onto→suc
𝐵 → 𝐴 ≈ 𝐵)) |
57 | 1, 56 | biimtrid 241 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) |