Metamath Proof Explorer


Theorem infpssrlem4

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Hypotheses infpssrlem.a ( 𝜑𝐵𝐴 )
infpssrlem.c ( 𝜑𝐹 : 𝐵1-1-onto𝐴 )
infpssrlem.d ( 𝜑𝐶 ∈ ( 𝐴𝐵 ) )
infpssrlem.e 𝐺 = ( rec ( 𝐹 , 𝐶 ) ↾ ω )
Assertion infpssrlem4 ( ( 𝜑𝑀 ∈ ω ∧ 𝑁𝑀 ) → ( 𝐺𝑀 ) ≠ ( 𝐺𝑁 ) )

Proof

Step Hyp Ref Expression
1 infpssrlem.a ( 𝜑𝐵𝐴 )
2 infpssrlem.c ( 𝜑𝐹 : 𝐵1-1-onto𝐴 )
3 infpssrlem.d ( 𝜑𝐶 ∈ ( 𝐴𝐵 ) )
4 infpssrlem.e 𝐺 = ( rec ( 𝐹 , 𝐶 ) ↾ ω )
5 fveq2 ( 𝑐 = ∅ → ( 𝐺𝑐 ) = ( 𝐺 ‘ ∅ ) )
6 5 neeq1d ( 𝑐 = ∅ → ( ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺 ‘ ∅ ) ≠ ( 𝐺𝑏 ) ) )
7 6 raleqbi1dv ( 𝑐 = ∅ → ( ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ∀ 𝑏 ∈ ∅ ( 𝐺 ‘ ∅ ) ≠ ( 𝐺𝑏 ) ) )
8 7 imbi2d ( 𝑐 = ∅ → ( ( 𝜑 → ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝜑 → ∀ 𝑏 ∈ ∅ ( 𝐺 ‘ ∅ ) ≠ ( 𝐺𝑏 ) ) ) )
9 fveq2 ( 𝑐 = 𝑑 → ( 𝐺𝑐 ) = ( 𝐺𝑑 ) )
10 9 neeq1d ( 𝑐 = 𝑑 → ( ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) )
11 10 raleqbi1dv ( 𝑐 = 𝑑 → ( ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) )
12 11 imbi2d ( 𝑐 = 𝑑 → ( ( 𝜑 → ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝜑 → ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ) )
13 fveq2 ( 𝑐 = suc 𝑑 → ( 𝐺𝑐 ) = ( 𝐺 ‘ suc 𝑑 ) )
14 13 neeq1d ( 𝑐 = suc 𝑑 → ( ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) )
15 14 raleqbi1dv ( 𝑐 = suc 𝑑 → ( ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) )
16 15 imbi2d ( 𝑐 = suc 𝑑 → ( ( 𝜑 → ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝜑 → ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) ) )
17 fveq2 ( 𝑐 = 𝑀 → ( 𝐺𝑐 ) = ( 𝐺𝑀 ) )
18 17 neeq1d ( 𝑐 = 𝑀 → ( ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) ) )
19 18 raleqbi1dv ( 𝑐 = 𝑀 → ( ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ↔ ∀ 𝑏𝑀 ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) ) )
20 19 imbi2d ( 𝑐 = 𝑀 → ( ( 𝜑 → ∀ 𝑏𝑐 ( 𝐺𝑐 ) ≠ ( 𝐺𝑏 ) ) ↔ ( 𝜑 → ∀ 𝑏𝑀 ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) ) ) )
21 ral0 𝑏 ∈ ∅ ( 𝐺 ‘ ∅ ) ≠ ( 𝐺𝑏 )
22 21 a1i ( 𝜑 → ∀ 𝑏 ∈ ∅ ( 𝐺 ‘ ∅ ) ≠ ( 𝐺𝑏 ) )
23 f1ocnv ( 𝐹 : 𝐵1-1-onto𝐴 𝐹 : 𝐴1-1-onto𝐵 )
24 f1of ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 : 𝐴𝐵 )
25 2 23 24 3syl ( 𝜑 𝐹 : 𝐴𝐵 )
26 25 adantl ( ( 𝑑 ∈ ω ∧ 𝜑 ) → 𝐹 : 𝐴𝐵 )
27 1 2 3 4 infpssrlem3 ( 𝜑𝐺 : ω ⟶ 𝐴 )
28 27 ffvelrnda ( ( 𝜑𝑑 ∈ ω ) → ( 𝐺𝑑 ) ∈ 𝐴 )
29 28 ancoms ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐺𝑑 ) ∈ 𝐴 )
30 26 29 ffvelrnd ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝐺𝑑 ) ) ∈ 𝐵 )
31 3 eldifbd ( 𝜑 → ¬ 𝐶𝐵 )
32 31 adantl ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ¬ 𝐶𝐵 )
33 nelne2 ( ( ( 𝐹 ‘ ( 𝐺𝑑 ) ) ∈ 𝐵 ∧ ¬ 𝐶𝐵 ) → ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ 𝐶 )
34 30 32 33 syl2anc ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ 𝐶 )
35 1 2 3 4 infpssrlem2 ( 𝑑 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) = ( 𝐹 ‘ ( 𝐺𝑑 ) ) )
36 35 adantr ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐺 ‘ suc 𝑑 ) = ( 𝐹 ‘ ( 𝐺𝑑 ) ) )
37 1 2 3 4 infpssrlem1 ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 )
38 37 adantl ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐺 ‘ ∅ ) = 𝐶 )
39 34 36 38 3netr4d ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ ∅ ) )
40 39 3adant3 ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ ∅ ) )
41 5 neeq2d ( 𝑐 = ∅ → ( ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ↔ ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ ∅ ) ) )
42 40 41 syl5ibr ( 𝑐 = ∅ → ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) )
43 42 adantrd ( 𝑐 = ∅ → ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) )
44 simpr ( ( 𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑 ) → 𝑐 ∈ suc 𝑑 )
45 peano2 ( 𝑑 ∈ ω → suc 𝑑 ∈ ω )
46 45 adantr ( ( 𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑 ) → suc 𝑑 ∈ ω )
47 elnn ( ( 𝑐 ∈ suc 𝑑 ∧ suc 𝑑 ∈ ω ) → 𝑐 ∈ ω )
48 44 46 47 syl2anc ( ( 𝑑 ∈ ω ∧ 𝑐 ∈ suc 𝑑 ) → 𝑐 ∈ ω )
49 48 3ad2antl1 ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → 𝑐 ∈ ω )
50 49 adantl ( ( 𝑐 ≠ ∅ ∧ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ) → 𝑐 ∈ ω )
51 simpl ( ( 𝑐 ≠ ∅ ∧ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ) → 𝑐 ≠ ∅ )
52 nnsuc ( ( 𝑐 ∈ ω ∧ 𝑐 ≠ ∅ ) → ∃ 𝑏 ∈ ω 𝑐 = suc 𝑏 )
53 50 51 52 syl2anc ( ( 𝑐 ≠ ∅ ∧ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ) → ∃ 𝑏 ∈ ω 𝑐 = suc 𝑏 )
54 nfv 𝑏 𝑑 ∈ ω
55 nfv 𝑏 𝜑
56 nfra1 𝑏𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 )
57 54 55 56 nf3an 𝑏 ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) )
58 nfv 𝑏 𝑐 ∈ suc 𝑑
59 57 58 nfan 𝑏 ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 )
60 nfv 𝑏 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 )
61 simpl3 ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) )
62 simpr ( ( 𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑 ) → suc 𝑏 ∈ suc 𝑑 )
63 nnord ( 𝑑 ∈ ω → Ord 𝑑 )
64 63 adantr ( ( 𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑 ) → Ord 𝑑 )
65 ordsucelsuc ( Ord 𝑑 → ( 𝑏𝑑 ↔ suc 𝑏 ∈ suc 𝑑 ) )
66 64 65 syl ( ( 𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑 ) → ( 𝑏𝑑 ↔ suc 𝑏 ∈ suc 𝑑 ) )
67 62 66 mpbird ( ( 𝑑 ∈ ω ∧ suc 𝑏 ∈ suc 𝑑 ) → 𝑏𝑑 )
68 67 3ad2antl1 ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ suc 𝑏 ∈ suc 𝑑 ) → 𝑏𝑑 )
69 68 adantrr ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → 𝑏𝑑 )
70 rsp ( ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ( 𝑏𝑑 → ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) )
71 61 69 70 sylc ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) )
72 f1of1 ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 : 𝐴1-1𝐵 )
73 2 23 72 3syl ( 𝜑 𝐹 : 𝐴1-1𝐵 )
74 73 ad2antlr ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → 𝐹 : 𝐴1-1𝐵 )
75 29 adantr ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( 𝐺𝑑 ) ∈ 𝐴 )
76 27 ffvelrnda ( ( 𝜑𝑏 ∈ ω ) → ( 𝐺𝑏 ) ∈ 𝐴 )
77 76 adantll ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( 𝐺𝑏 ) ∈ 𝐴 )
78 f1fveq ( ( 𝐹 : 𝐴1-1𝐵 ∧ ( ( 𝐺𝑑 ) ∈ 𝐴 ∧ ( 𝐺𝑏 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝐺𝑑 ) ) = ( 𝐹 ‘ ( 𝐺𝑏 ) ) ↔ ( 𝐺𝑑 ) = ( 𝐺𝑏 ) ) )
79 74 75 77 78 syl12anc ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( ( 𝐹 ‘ ( 𝐺𝑑 ) ) = ( 𝐹 ‘ ( 𝐺𝑏 ) ) ↔ ( 𝐺𝑑 ) = ( 𝐺𝑏 ) ) )
80 79 necon3bid ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ ( 𝐹 ‘ ( 𝐺𝑏 ) ) ↔ ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) )
81 80 biimprd ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ ( 𝐹 ‘ ( 𝐺𝑏 ) ) ) )
82 35 adantr ( ( 𝑑 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝐺 ‘ suc 𝑑 ) = ( 𝐹 ‘ ( 𝐺𝑑 ) ) )
83 1 2 3 4 infpssrlem2 ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑏 ) = ( 𝐹 ‘ ( 𝐺𝑏 ) ) )
84 83 adantl ( ( 𝑑 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝐺 ‘ suc 𝑏 ) = ( 𝐹 ‘ ( 𝐺𝑏 ) ) )
85 82 84 neeq12d ( ( 𝑑 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ↔ ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ ( 𝐹 ‘ ( 𝐺𝑏 ) ) ) )
86 85 adantlr ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ↔ ( 𝐹 ‘ ( 𝐺𝑑 ) ) ≠ ( 𝐹 ‘ ( 𝐺𝑏 ) ) ) )
87 81 86 sylibrd ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ 𝑏 ∈ ω ) → ( ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) )
88 87 adantrl ( ( ( 𝑑 ∈ ω ∧ 𝜑 ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → ( ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) )
89 88 3adantl3 ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → ( ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) )
90 71 89 mpd ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ ( suc 𝑏 ∈ suc 𝑑𝑏 ∈ ω ) ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) )
91 90 expr ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ suc 𝑏 ∈ suc 𝑑 ) → ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) )
92 eleq1 ( 𝑐 = suc 𝑏 → ( 𝑐 ∈ suc 𝑑 ↔ suc 𝑏 ∈ suc 𝑑 ) )
93 92 anbi2d ( 𝑐 = suc 𝑏 → ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ↔ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ suc 𝑏 ∈ suc 𝑑 ) ) )
94 fveq2 ( 𝑐 = suc 𝑏 → ( 𝐺𝑐 ) = ( 𝐺 ‘ suc 𝑏 ) )
95 94 neeq2d ( 𝑐 = suc 𝑏 → ( ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ↔ ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) )
96 95 imbi2d ( 𝑐 = suc 𝑏 → ( ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) ↔ ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) ) )
97 93 96 imbi12d ( 𝑐 = suc 𝑏 → ( ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) ) ↔ ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ suc 𝑏 ∈ suc 𝑑 ) → ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺 ‘ suc 𝑏 ) ) ) ) )
98 91 97 mpbiri ( 𝑐 = suc 𝑏 → ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝑏 ∈ ω → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) ) )
99 98 com3l ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝑏 ∈ ω → ( 𝑐 = suc 𝑏 → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) ) )
100 59 60 99 rexlimd ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( ∃ 𝑏 ∈ ω 𝑐 = suc 𝑏 → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) )
101 100 adantl ( ( 𝑐 ≠ ∅ ∧ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ) → ( ∃ 𝑏 ∈ ω 𝑐 = suc 𝑏 → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) )
102 53 101 mpd ( ( 𝑐 ≠ ∅ ∧ ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) )
103 102 ex ( 𝑐 ≠ ∅ → ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ) )
104 43 103 pm2.61ine ( ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) ∧ 𝑐 ∈ suc 𝑑 ) → ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) )
105 104 ralrimiva ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) → ∀ 𝑐 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) )
106 fveq2 ( 𝑐 = 𝑏 → ( 𝐺𝑐 ) = ( 𝐺𝑏 ) )
107 106 neeq2d ( 𝑐 = 𝑏 → ( ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ↔ ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) )
108 107 cbvralvw ( ∀ 𝑐 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑐 ) ↔ ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) )
109 105 108 sylib ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) → ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) )
110 109 3exp ( 𝑑 ∈ ω → ( 𝜑 → ( ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) → ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) ) )
111 110 a2d ( 𝑑 ∈ ω → ( ( 𝜑 → ∀ 𝑏𝑑 ( 𝐺𝑑 ) ≠ ( 𝐺𝑏 ) ) → ( 𝜑 → ∀ 𝑏 ∈ suc 𝑑 ( 𝐺 ‘ suc 𝑑 ) ≠ ( 𝐺𝑏 ) ) ) )
112 8 12 16 20 22 111 finds ( 𝑀 ∈ ω → ( 𝜑 → ∀ 𝑏𝑀 ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) ) )
113 112 impcom ( ( 𝜑𝑀 ∈ ω ) → ∀ 𝑏𝑀 ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) )
114 fveq2 ( 𝑏 = 𝑁 → ( 𝐺𝑏 ) = ( 𝐺𝑁 ) )
115 114 neeq2d ( 𝑏 = 𝑁 → ( ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) ↔ ( 𝐺𝑀 ) ≠ ( 𝐺𝑁 ) ) )
116 115 rspccv ( ∀ 𝑏𝑀 ( 𝐺𝑀 ) ≠ ( 𝐺𝑏 ) → ( 𝑁𝑀 → ( 𝐺𝑀 ) ≠ ( 𝐺𝑁 ) ) )
117 113 116 syl ( ( 𝜑𝑀 ∈ ω ) → ( 𝑁𝑀 → ( 𝐺𝑀 ) ≠ ( 𝐺𝑁 ) ) )
118 117 3impia ( ( 𝜑𝑀 ∈ ω ∧ 𝑁𝑀 ) → ( 𝐺𝑀 ) ≠ ( 𝐺𝑁 ) )