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 |
⊢ ( ( 𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀 ) → ( 𝐺 ‘ 𝑀 ) ≠ ( 𝐺 ‘ 𝑁 ) ) |