This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ω ) → ( 𝐺 ‘ 𝑑 ) ∈ 𝐴 )
29 28 ancoms ⊢ ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( 𝐺 ‘ 𝑑 ) ∈ 𝐴 )
30 26 29 ffvelcdmd ⊢ ( ( 𝑑 ∈ ω ∧ 𝜑 ) → ( ◡ 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) ∈ 𝐵 )
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 imbitrrid ⊢ ( 𝑐 = ∅ → ( ( 𝑑 ∈ ω ∧ 𝜑 ∧ ∀ 𝑏 ∈ 𝑑 ( 𝐺 ‘ 𝑑 ) ≠ ( 𝐺 ‘ 𝑏 ) ) → ( 𝐺 ‘ 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ω ) → ( 𝐺 ‘ 𝑏 ) ∈ 𝐴 )
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 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀 ) → ( 𝐺 ‘ 𝑀 ) ≠ ( 𝐺 ‘ 𝑁 ) )