Step | Hyp | Ref
| Expression |
1 | | peano2 4579 |
. . . . . 6
⊢ (𝐵 ∈ ω → suc 𝐵 ∈
ω) |
2 | 1 | adantl 275 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → suc
𝐵 ∈
ω) |
3 | | brdomg 6726 |
. . . . 5
⊢ (suc
𝐵 ∈ ω →
(suc 𝐴 ≼ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴–1-1→suc 𝐵)) |
4 | 2, 3 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ≼ suc 𝐵 ↔ ∃𝑓 𝑓:suc 𝐴–1-1→suc 𝐵)) |
5 | 4 | biimpa 294 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) → ∃𝑓 𝑓:suc 𝐴–1-1→suc 𝐵) |
6 | | simpr 109 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝑓:suc 𝐴–1-1→suc 𝐵) |
7 | 2 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → suc 𝐵 ∈ ω) |
8 | | sssucid 4400 |
. . . . . . . 8
⊢ 𝐴 ⊆ suc 𝐴 |
9 | 8 | a1i 9 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ⊆ suc 𝐴) |
10 | | simplll 528 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ∈ ω) |
11 | | f1imaen2g 6771 |
. . . . . . 7
⊢ (((𝑓:suc 𝐴–1-1→suc 𝐵 ∧ suc 𝐵 ∈ ω) ∧ (𝐴 ⊆ suc 𝐴 ∧ 𝐴 ∈ ω)) → (𝑓 “ 𝐴) ≈ 𝐴) |
12 | 6, 7, 9, 10, 11 | syl22anc 1234 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ 𝐴) ≈ 𝐴) |
13 | 12 | ensymd 6761 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ≈ (𝑓 “ 𝐴)) |
14 | | difexg 4130 |
. . . . . . 7
⊢ (suc
𝐵 ∈ ω →
(suc 𝐵 ∖ {(𝑓‘𝐴)}) ∈ V) |
15 | 7, 14 | syl 14 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (suc 𝐵 ∖ {(𝑓‘𝐴)}) ∈ V) |
16 | | nnord 4596 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → Ord 𝐴) |
17 | | orddif 4531 |
. . . . . . . . . 10
⊢ (Ord
𝐴 → 𝐴 = (suc 𝐴 ∖ {𝐴})) |
18 | 16, 17 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → 𝐴 = (suc 𝐴 ∖ {𝐴})) |
19 | 18 | imaeq2d 4953 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝑓 “ 𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴}))) |
20 | 10, 19 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ 𝐴) = (𝑓 “ (suc 𝐴 ∖ {𝐴}))) |
21 | | f1fn 5405 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–1-1→suc 𝐵 → 𝑓 Fn suc 𝐴) |
22 | 21 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝑓 Fn suc 𝐴) |
23 | | sucidg 4401 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → 𝐴 ∈ suc 𝐴) |
24 | 10, 23 | syl 14 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ∈ suc 𝐴) |
25 | | fnsnfv 5555 |
. . . . . . . . . . 11
⊢ ((𝑓 Fn suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
26 | 22, 24, 25 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
27 | 26 | difeq2d 3245 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → ((𝑓 “ suc 𝐴) ∖ {(𝑓‘𝐴)}) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
28 | | df-f1 5203 |
. . . . . . . . . . . 12
⊢ (𝑓:suc 𝐴–1-1→suc 𝐵 ↔ (𝑓:suc 𝐴⟶suc 𝐵 ∧ Fun ◡𝑓)) |
29 | 28 | simprbi 273 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1→suc 𝐵 → Fun ◡𝑓) |
30 | | imadif 5278 |
. . . . . . . . . . 11
⊢ (Fun
◡𝑓 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
31 | 29, 30 | syl 14 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴–1-1→suc 𝐵 → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
32 | 31 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) = ((𝑓 “ suc 𝐴) ∖ (𝑓 “ {𝐴}))) |
33 | 27, 32 | eqtr4d 2206 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → ((𝑓 “ suc 𝐴) ∖ {(𝑓‘𝐴)}) = (𝑓 “ (suc 𝐴 ∖ {𝐴}))) |
34 | | f1f 5403 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴–1-1→suc 𝐵 → 𝑓:suc 𝐴⟶suc 𝐵) |
35 | 34 | adantl 275 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝑓:suc 𝐴⟶suc 𝐵) |
36 | | imassrn 4964 |
. . . . . . . . . . 11
⊢ (𝑓 “ suc 𝐴) ⊆ ran 𝑓 |
37 | | frn 5356 |
. . . . . . . . . . 11
⊢ (𝑓:suc 𝐴⟶suc 𝐵 → ran 𝑓 ⊆ suc 𝐵) |
38 | 36, 37 | sstrid 3158 |
. . . . . . . . . 10
⊢ (𝑓:suc 𝐴⟶suc 𝐵 → (𝑓 “ suc 𝐴) ⊆ suc 𝐵) |
39 | 35, 38 | syl 14 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ suc 𝐴) ⊆ suc 𝐵) |
40 | 39 | ssdifd 3263 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → ((𝑓 “ suc 𝐴) ∖ {(𝑓‘𝐴)}) ⊆ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
41 | 33, 40 | eqsstrrd 3184 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ (suc 𝐴 ∖ {𝐴})) ⊆ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
42 | 20, 41 | eqsstrd 3183 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ 𝐴) ⊆ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
43 | | ssdomg 6756 |
. . . . . 6
⊢ ((suc
𝐵 ∖ {(𝑓‘𝐴)}) ∈ V → ((𝑓 “ 𝐴) ⊆ (suc 𝐵 ∖ {(𝑓‘𝐴)}) → (𝑓 “ 𝐴) ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)}))) |
44 | 15, 42, 43 | sylc 62 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓 “ 𝐴) ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
45 | | endomtr 6768 |
. . . . 5
⊢ ((𝐴 ≈ (𝑓 “ 𝐴) ∧ (𝑓 “ 𝐴) ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)})) → 𝐴 ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
46 | 13, 44, 45 | syl2anc 409 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
47 | | simpllr 529 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐵 ∈ ω) |
48 | 35, 24 | ffvelrnd 5632 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (𝑓‘𝐴) ∈ suc 𝐵) |
49 | | phplem3g 6834 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ (𝑓‘𝐴) ∈ suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
50 | 47, 48, 49 | syl2anc 409 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐵 ≈ (suc 𝐵 ∖ {(𝑓‘𝐴)})) |
51 | 50 | ensymd 6761 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵) |
52 | | domentr 6769 |
. . . 4
⊢ ((𝐴 ≼ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ∧ (suc 𝐵 ∖ {(𝑓‘𝐴)}) ≈ 𝐵) → 𝐴 ≼ 𝐵) |
53 | 46, 51, 52 | syl2anc 409 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) ∧ 𝑓:suc 𝐴–1-1→suc 𝐵) → 𝐴 ≼ 𝐵) |
54 | 5, 53 | exlimddv 1891 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc 𝐴 ≼ suc 𝐵) → 𝐴 ≼ 𝐵) |
55 | 54 | ex 114 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ≼ suc 𝐵 → 𝐴 ≼ 𝐵)) |