| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑐 = ∅ → (𝐺‘𝑐) = (𝐺‘∅)) | 
| 2 | 1 | neeq1d 3000 | . . . . . . 7
⊢ (𝑐 = ∅ → ((𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ (𝐺‘∅) ≠ (𝐺‘𝑏))) | 
| 3 | 2 | raleqbi1dv 3338 | . . . . . 6
⊢ (𝑐 = ∅ → (∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ ∀𝑏 ∈ ∅ (𝐺‘∅) ≠ (𝐺‘𝑏))) | 
| 4 | 3 | imbi2d 340 | . . . . 5
⊢ (𝑐 = ∅ → ((𝜑 → ∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏)) ↔ (𝜑 → ∀𝑏 ∈ ∅ (𝐺‘∅) ≠ (𝐺‘𝑏)))) | 
| 5 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑐 = 𝑑 → (𝐺‘𝑐) = (𝐺‘𝑑)) | 
| 6 | 5 | neeq1d 3000 | . . . . . . 7
⊢ (𝑐 = 𝑑 → ((𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑑) ≠ (𝐺‘𝑏))) | 
| 7 | 6 | raleqbi1dv 3338 | . . . . . 6
⊢ (𝑐 = 𝑑 → (∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏))) | 
| 8 | 7 | imbi2d 340 | . . . . 5
⊢ (𝑐 = 𝑑 → ((𝜑 → ∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏)) ↔ (𝜑 → ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)))) | 
| 9 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑐 = suc 𝑑 → (𝐺‘𝑐) = (𝐺‘suc 𝑑)) | 
| 10 | 9 | neeq1d 3000 | . . . . . . 7
⊢ (𝑐 = suc 𝑑 → ((𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ (𝐺‘suc 𝑑) ≠ (𝐺‘𝑏))) | 
| 11 | 10 | raleqbi1dv 3338 | . . . . . 6
⊢ (𝑐 = suc 𝑑 → (∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏))) | 
| 12 | 11 | imbi2d 340 | . . . . 5
⊢ (𝑐 = suc 𝑑 → ((𝜑 → ∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏)) ↔ (𝜑 → ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏)))) | 
| 13 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑐 = 𝑀 → (𝐺‘𝑐) = (𝐺‘𝑀)) | 
| 14 | 13 | neeq1d 3000 | . . . . . . 7
⊢ (𝑐 = 𝑀 → ((𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑀) ≠ (𝐺‘𝑏))) | 
| 15 | 14 | raleqbi1dv 3338 | . . . . . 6
⊢ (𝑐 = 𝑀 → (∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏) ↔ ∀𝑏 ∈ 𝑀 (𝐺‘𝑀) ≠ (𝐺‘𝑏))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑐 = 𝑀 → ((𝜑 → ∀𝑏 ∈ 𝑐 (𝐺‘𝑐) ≠ (𝐺‘𝑏)) ↔ (𝜑 → ∀𝑏 ∈ 𝑀 (𝐺‘𝑀) ≠ (𝐺‘𝑏)))) | 
| 17 |  | ral0 4513 | . . . . . 6
⊢
∀𝑏 ∈
∅ (𝐺‘∅)
≠ (𝐺‘𝑏) | 
| 18 | 17 | a1i 11 | . . . . 5
⊢ (𝜑 → ∀𝑏 ∈ ∅ (𝐺‘∅) ≠ (𝐺‘𝑏)) | 
| 19 |  | infpssrlem.c | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) | 
| 20 |  | f1ocnv 6860 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐵) | 
| 21 |  | f1of 6848 | . . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐴⟶𝐵) | 
| 22 | 19, 20, 21 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹:𝐴⟶𝐵) | 
| 23 | 22 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ ω ∧ 𝜑) → ◡𝐹:𝐴⟶𝐵) | 
| 24 |  | infpssrlem.a | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ⊆ 𝐴) | 
| 25 |  | infpssrlem.d | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) | 
| 26 |  | infpssrlem.e | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) | 
| 27 | 24, 19, 25, 26 | infpssrlem3 10345 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺:ω⟶𝐴) | 
| 28 | 27 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ ω) → (𝐺‘𝑑) ∈ 𝐴) | 
| 29 | 28 | ancoms 458 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (𝐺‘𝑑) ∈ 𝐴) | 
| 30 | 23, 29 | ffvelcdmd 7105 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (◡𝐹‘(𝐺‘𝑑)) ∈ 𝐵) | 
| 31 | 25 | eldifbd 3964 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | 
| 32 | 31 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ω ∧ 𝜑) → ¬ 𝐶 ∈ 𝐵) | 
| 33 |  | nelne2 3040 | . . . . . . . . . . . . . . 15
⊢ (((◡𝐹‘(𝐺‘𝑑)) ∈ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → (◡𝐹‘(𝐺‘𝑑)) ≠ 𝐶) | 
| 34 | 30, 32, 33 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (◡𝐹‘(𝐺‘𝑑)) ≠ 𝐶) | 
| 35 | 24, 19, 25, 26 | infpssrlem2 10344 | . . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ ω → (𝐺‘suc 𝑑) = (◡𝐹‘(𝐺‘𝑑))) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (𝐺‘suc 𝑑) = (◡𝐹‘(𝐺‘𝑑))) | 
| 37 | 24, 19, 25, 26 | infpssrlem1 10343 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘∅) = 𝐶) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (𝐺‘∅) = 𝐶) | 
| 39 | 34, 36, 38 | 3netr4d 3018 | . . . . . . . . . . . . 13
⊢ ((𝑑 ∈ ω ∧ 𝜑) → (𝐺‘suc 𝑑) ≠ (𝐺‘∅)) | 
| 40 | 39 | 3adant3 1133 | . . . . . . . . . . . 12
⊢ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) → (𝐺‘suc 𝑑) ≠ (𝐺‘∅)) | 
| 41 | 1 | neeq2d 3001 | . . . . . . . . . . . 12
⊢ (𝑐 = ∅ → ((𝐺‘suc 𝑑) ≠ (𝐺‘𝑐) ↔ (𝐺‘suc 𝑑) ≠ (𝐺‘∅))) | 
| 42 | 40, 41 | imbitrrid 246 | . . . . . . . . . . 11
⊢ (𝑐 = ∅ → ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) | 
| 43 | 42 | adantrd 491 | . . . . . . . . . 10
⊢ (𝑐 = ∅ → (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) | 
| 44 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑) → 𝑐 ∈ suc 𝑑) | 
| 45 |  | peano2 7912 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ ω → suc 𝑑 ∈
ω) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑) → suc 𝑑 ∈ ω) | 
| 47 |  | elnn 7898 | . . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ suc 𝑑 ∧ suc 𝑑 ∈ ω) → 𝑐 ∈ ω) | 
| 48 | 44, 46, 47 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑) → 𝑐 ∈ ω) | 
| 49 | 48 | 3ad2antl1 1186 | . . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → 𝑐 ∈ ω) | 
| 50 | 49 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑐 ≠ ∅ ∧ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑)) → 𝑐 ∈ ω) | 
| 51 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑐 ≠ ∅ ∧ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑)) → 𝑐 ≠ ∅) | 
| 52 |  | nnsuc 7905 | . . . . . . . . . . . . 13
⊢ ((𝑐 ∈ ω ∧ 𝑐 ≠ ∅) →
∃𝑏 ∈ ω
𝑐 = suc 𝑏) | 
| 53 | 50, 51, 52 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑐 ≠ ∅ ∧ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑)) → ∃𝑏 ∈ ω 𝑐 = suc 𝑏) | 
| 54 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏 𝑑 ∈ ω | 
| 55 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏𝜑 | 
| 56 |  | nfra1 3284 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑏∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏) | 
| 57 | 54, 55, 56 | nf3an 1901 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏(𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) | 
| 58 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑏 𝑐 ∈ suc 𝑑 | 
| 59 | 57, 58 | nfan 1899 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑏((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) | 
| 60 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑏(𝐺‘suc 𝑑) ≠ (𝐺‘𝑐) | 
| 61 |  | simpl3 1194 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) | 
| 62 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑) → suc 𝑏 ∈ suc 𝑑) | 
| 63 |  | nnord 7895 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 ∈ ω → Ord 𝑑) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑) → Ord 𝑑) | 
| 65 |  | ordsucelsuc 7842 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
𝑑 → (𝑏 ∈ 𝑑 ↔ suc 𝑏 ∈ suc 𝑑)) | 
| 66 | 64, 65 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑) → (𝑏 ∈ 𝑑 ↔ suc 𝑏 ∈ suc 𝑑)) | 
| 67 | 62, 66 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑) → 𝑏 ∈ 𝑑) | 
| 68 | 67 | 3ad2antl1 1186 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ suc 𝑏 ∈ suc 𝑑) → 𝑏 ∈ 𝑑) | 
| 69 | 68 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → 𝑏 ∈ 𝑑) | 
| 70 |  | rsp 3247 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏 ∈
𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏) → (𝑏 ∈ 𝑑 → (𝐺‘𝑑) ≠ (𝐺‘𝑏))) | 
| 71 | 61, 69, 70 | sylc 65 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → (𝐺‘𝑑) ≠ (𝐺‘𝑏)) | 
| 72 |  | f1of1 6847 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (◡𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐴–1-1→𝐵) | 
| 73 | 19, 20, 72 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ◡𝐹:𝐴–1-1→𝐵) | 
| 74 | 73 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ◡𝐹:𝐴–1-1→𝐵) | 
| 75 | 29 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → (𝐺‘𝑑) ∈ 𝐴) | 
| 76 | 27 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑏 ∈ ω) → (𝐺‘𝑏) ∈ 𝐴) | 
| 77 | 76 | adantll 714 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → (𝐺‘𝑏) ∈ 𝐴) | 
| 78 |  | f1fveq 7282 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((◡𝐹:𝐴–1-1→𝐵 ∧ ((𝐺‘𝑑) ∈ 𝐴 ∧ (𝐺‘𝑏) ∈ 𝐴)) → ((◡𝐹‘(𝐺‘𝑑)) = (◡𝐹‘(𝐺‘𝑏)) ↔ (𝐺‘𝑑) = (𝐺‘𝑏))) | 
| 79 | 74, 75, 77, 78 | syl12anc 837 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ((◡𝐹‘(𝐺‘𝑑)) = (◡𝐹‘(𝐺‘𝑏)) ↔ (𝐺‘𝑑) = (𝐺‘𝑏))) | 
| 80 | 79 | necon3bid 2985 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ((◡𝐹‘(𝐺‘𝑑)) ≠ (◡𝐹‘(𝐺‘𝑏)) ↔ (𝐺‘𝑑) ≠ (𝐺‘𝑏))) | 
| 81 | 80 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ((𝐺‘𝑑) ≠ (𝐺‘𝑏) → (◡𝐹‘(𝐺‘𝑑)) ≠ (◡𝐹‘(𝐺‘𝑏)))) | 
| 82 | 35 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 ∈ ω ∧ 𝑏 ∈ ω) → (𝐺‘suc 𝑑) = (◡𝐹‘(𝐺‘𝑑))) | 
| 83 | 24, 19, 25, 26 | infpssrlem2 10344 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ ω → (𝐺‘suc 𝑏) = (◡𝐹‘(𝐺‘𝑏))) | 
| 84 | 83 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑑 ∈ ω ∧ 𝑏 ∈ ω) → (𝐺‘suc 𝑏) = (◡𝐹‘(𝐺‘𝑏))) | 
| 85 | 82, 84 | neeq12d 3002 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ∈ ω ∧ 𝑏 ∈ ω) → ((𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏) ↔ (◡𝐹‘(𝐺‘𝑑)) ≠ (◡𝐹‘(𝐺‘𝑏)))) | 
| 86 | 85 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ((𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏) ↔ (◡𝐹‘(𝐺‘𝑑)) ≠ (◡𝐹‘(𝐺‘𝑏)))) | 
| 87 | 81, 86 | sylibrd 259 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ 𝑏 ∈ ω) → ((𝐺‘𝑑) ≠ (𝐺‘𝑏) → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))) | 
| 88 | 87 | adantrl 716 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 ∈ ω ∧ 𝜑) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → ((𝐺‘𝑑) ≠ (𝐺‘𝑏) → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))) | 
| 89 | 88 | 3adantl3 1169 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → ((𝐺‘𝑑) ≠ (𝐺‘𝑏) → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))) | 
| 90 | 71, 89 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ (suc 𝑏 ∈ suc 𝑑 ∧ 𝑏 ∈ ω)) → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏)) | 
| 91 | 90 | expr 456 | . . . . . . . . . . . . . . . 16
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ suc 𝑏 ∈ suc 𝑑) → (𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))) | 
| 92 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = suc 𝑏 → (𝑐 ∈ suc 𝑑 ↔ suc 𝑏 ∈ suc 𝑑)) | 
| 93 | 92 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 = suc 𝑏 → (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) ↔ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ suc 𝑏 ∈ suc 𝑑))) | 
| 94 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = suc 𝑏 → (𝐺‘𝑐) = (𝐺‘suc 𝑏)) | 
| 95 | 94 | neeq2d 3001 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = suc 𝑏 → ((𝐺‘suc 𝑑) ≠ (𝐺‘𝑐) ↔ (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))) | 
| 96 | 95 | imbi2d 340 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 = suc 𝑏 → ((𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)) ↔ (𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏)))) | 
| 97 | 93, 96 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = suc 𝑏 → ((((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) ↔ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ suc 𝑏 ∈ suc 𝑑) → (𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘suc 𝑏))))) | 
| 98 | 91, 97 | mpbiri 258 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = suc 𝑏 → (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝑏 ∈ ω → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)))) | 
| 99 | 98 | com3l 89 | . . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝑏 ∈ ω → (𝑐 = suc 𝑏 → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)))) | 
| 100 | 59, 60, 99 | rexlimd 3266 | . . . . . . . . . . . . 13
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (∃𝑏 ∈ ω 𝑐 = suc 𝑏 → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) | 
| 101 | 100 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑐 ≠ ∅ ∧ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑)) → (∃𝑏 ∈ ω 𝑐 = suc 𝑏 → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) | 
| 102 | 53, 101 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝑐 ≠ ∅ ∧ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑)) → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)) | 
| 103 | 102 | ex 412 | . . . . . . . . . 10
⊢ (𝑐 ≠ ∅ → (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐))) | 
| 104 | 43, 103 | pm2.61ine 3025 | . . . . . . . . 9
⊢ (((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) ∧ 𝑐 ∈ suc 𝑑) → (𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)) | 
| 105 | 104 | ralrimiva 3146 | . . . . . . . 8
⊢ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) → ∀𝑐 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑐)) | 
| 106 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑐 = 𝑏 → (𝐺‘𝑐) = (𝐺‘𝑏)) | 
| 107 | 106 | neeq2d 3001 | . . . . . . . . 9
⊢ (𝑐 = 𝑏 → ((𝐺‘suc 𝑑) ≠ (𝐺‘𝑐) ↔ (𝐺‘suc 𝑑) ≠ (𝐺‘𝑏))) | 
| 108 | 107 | cbvralvw 3237 | . . . . . . . 8
⊢
(∀𝑐 ∈
suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑐) ↔ ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏)) | 
| 109 | 105, 108 | sylib 218 | . . . . . . 7
⊢ ((𝑑 ∈ ω ∧ 𝜑 ∧ ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) → ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏)) | 
| 110 | 109 | 3exp 1120 | . . . . . 6
⊢ (𝑑 ∈ ω → (𝜑 → (∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏) → ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏)))) | 
| 111 | 110 | a2d 29 | . . . . 5
⊢ (𝑑 ∈ ω → ((𝜑 → ∀𝑏 ∈ 𝑑 (𝐺‘𝑑) ≠ (𝐺‘𝑏)) → (𝜑 → ∀𝑏 ∈ suc 𝑑(𝐺‘suc 𝑑) ≠ (𝐺‘𝑏)))) | 
| 112 | 4, 8, 12, 16, 18, 111 | finds 7918 | . . . 4
⊢ (𝑀 ∈ ω → (𝜑 → ∀𝑏 ∈ 𝑀 (𝐺‘𝑀) ≠ (𝐺‘𝑏))) | 
| 113 | 112 | impcom 407 | . . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ω) → ∀𝑏 ∈ 𝑀 (𝐺‘𝑀) ≠ (𝐺‘𝑏)) | 
| 114 |  | fveq2 6906 | . . . . 5
⊢ (𝑏 = 𝑁 → (𝐺‘𝑏) = (𝐺‘𝑁)) | 
| 115 | 114 | neeq2d 3001 | . . . 4
⊢ (𝑏 = 𝑁 → ((𝐺‘𝑀) ≠ (𝐺‘𝑏) ↔ (𝐺‘𝑀) ≠ (𝐺‘𝑁))) | 
| 116 | 115 | rspccv 3619 | . . 3
⊢
(∀𝑏 ∈
𝑀 (𝐺‘𝑀) ≠ (𝐺‘𝑏) → (𝑁 ∈ 𝑀 → (𝐺‘𝑀) ≠ (𝐺‘𝑁))) | 
| 117 | 113, 116 | syl 17 | . 2
⊢ ((𝜑 ∧ 𝑀 ∈ ω) → (𝑁 ∈ 𝑀 → (𝐺‘𝑀) ≠ (𝐺‘𝑁))) | 
| 118 | 117 | 3impia 1118 | 1
⊢ ((𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀) → (𝐺‘𝑀) ≠ (𝐺‘𝑁)) |