# Metamath Proof Explorer

## Theorem infpssrlem4

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

Ref Expression
Hypotheses infpssrlem.a ${⊢}{\phi }\to {B}\subseteq {A}$
infpssrlem.c ${⊢}{\phi }\to {F}:{B}\underset{1-1 onto}{⟶}{A}$
infpssrlem.d ${⊢}{\phi }\to {C}\in \left({A}\setminus {B}\right)$
infpssrlem.e ${⊢}{G}={\mathrm{rec}\left({{F}}^{-1},{C}\right)↾}_{\mathrm{\omega }}$
Assertion infpssrlem4 ${⊢}\left({\phi }\wedge {M}\in \mathrm{\omega }\wedge {N}\in {M}\right)\to {G}\left({M}\right)\ne {G}\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 infpssrlem.a ${⊢}{\phi }\to {B}\subseteq {A}$
2 infpssrlem.c ${⊢}{\phi }\to {F}:{B}\underset{1-1 onto}{⟶}{A}$
3 infpssrlem.d ${⊢}{\phi }\to {C}\in \left({A}\setminus {B}\right)$
4 infpssrlem.e ${⊢}{G}={\mathrm{rec}\left({{F}}^{-1},{C}\right)↾}_{\mathrm{\omega }}$
5 fveq2 ${⊢}{c}=\varnothing \to {G}\left({c}\right)={G}\left(\varnothing \right)$
6 5 neeq1d ${⊢}{c}=\varnothing \to \left({G}\left({c}\right)\ne {G}\left({b}\right)↔{G}\left(\varnothing \right)\ne {G}\left({b}\right)\right)$
7 6 raleqbi1dv ${⊢}{c}=\varnothing \to \left(\forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)↔\forall {b}\in \varnothing \phantom{\rule{.4em}{0ex}}{G}\left(\varnothing \right)\ne {G}\left({b}\right)\right)$
8 7 imbi2d ${⊢}{c}=\varnothing \to \left(\left({\phi }\to \forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)\right)↔\left({\phi }\to \forall {b}\in \varnothing \phantom{\rule{.4em}{0ex}}{G}\left(\varnothing \right)\ne {G}\left({b}\right)\right)\right)$
9 fveq2 ${⊢}{c}={d}\to {G}\left({c}\right)={G}\left({d}\right)$
10 9 neeq1d ${⊢}{c}={d}\to \left({G}\left({c}\right)\ne {G}\left({b}\right)↔{G}\left({d}\right)\ne {G}\left({b}\right)\right)$
11 10 raleqbi1dv ${⊢}{c}={d}\to \left(\forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)↔\forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)$
12 11 imbi2d ${⊢}{c}={d}\to \left(\left({\phi }\to \forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)\right)↔\left({\phi }\to \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\right)$
13 fveq2 ${⊢}{c}=\mathrm{suc}{d}\to {G}\left({c}\right)={G}\left(\mathrm{suc}{d}\right)$
14 13 neeq1d ${⊢}{c}=\mathrm{suc}{d}\to \left({G}\left({c}\right)\ne {G}\left({b}\right)↔{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)$
15 14 raleqbi1dv ${⊢}{c}=\mathrm{suc}{d}\to \left(\forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)↔\forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)$
16 15 imbi2d ${⊢}{c}=\mathrm{suc}{d}\to \left(\left({\phi }\to \forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)\right)↔\left({\phi }\to \forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)\right)$
17 fveq2 ${⊢}{c}={M}\to {G}\left({c}\right)={G}\left({M}\right)$
18 17 neeq1d ${⊢}{c}={M}\to \left({G}\left({c}\right)\ne {G}\left({b}\right)↔{G}\left({M}\right)\ne {G}\left({b}\right)\right)$
19 18 raleqbi1dv ${⊢}{c}={M}\to \left(\forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)↔\forall {b}\in {M}\phantom{\rule{.4em}{0ex}}{G}\left({M}\right)\ne {G}\left({b}\right)\right)$
20 19 imbi2d ${⊢}{c}={M}\to \left(\left({\phi }\to \forall {b}\in {c}\phantom{\rule{.4em}{0ex}}{G}\left({c}\right)\ne {G}\left({b}\right)\right)↔\left({\phi }\to \forall {b}\in {M}\phantom{\rule{.4em}{0ex}}{G}\left({M}\right)\ne {G}\left({b}\right)\right)\right)$
21 ral0 ${⊢}\forall {b}\in \varnothing \phantom{\rule{.4em}{0ex}}{G}\left(\varnothing \right)\ne {G}\left({b}\right)$
22 21 a1i ${⊢}{\phi }\to \forall {b}\in \varnothing \phantom{\rule{.4em}{0ex}}{G}\left(\varnothing \right)\ne {G}\left({b}\right)$
23 f1ocnv ${⊢}{F}:{B}\underset{1-1 onto}{⟶}{A}\to {{F}}^{-1}:{A}\underset{1-1 onto}{⟶}{B}$
24 f1of ${⊢}{{F}}^{-1}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{A}⟶{B}$
25 2 23 24 3syl ${⊢}{\phi }\to {{F}}^{-1}:{A}⟶{B}$
26 25 adantl ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {{F}}^{-1}:{A}⟶{B}$
27 1 2 3 4 infpssrlem3 ${⊢}{\phi }\to {G}:\mathrm{\omega }⟶{A}$
28 27 ffvelrnda ${⊢}\left({\phi }\wedge {d}\in \mathrm{\omega }\right)\to {G}\left({d}\right)\in {A}$
29 28 ancoms ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {G}\left({d}\right)\in {A}$
30 26 29 ffvelrnd ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {{F}}^{-1}\left({G}\left({d}\right)\right)\in {B}$
31 3 eldifbd ${⊢}{\phi }\to ¬{C}\in {B}$
32 31 adantl ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to ¬{C}\in {B}$
33 nelne2 ${⊢}\left({{F}}^{-1}\left({G}\left({d}\right)\right)\in {B}\wedge ¬{C}\in {B}\right)\to {{F}}^{-1}\left({G}\left({d}\right)\right)\ne {C}$
34 30 32 33 syl2anc ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {{F}}^{-1}\left({G}\left({d}\right)\right)\ne {C}$
35 1 2 3 4 infpssrlem2 ${⊢}{d}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)={{F}}^{-1}\left({G}\left({d}\right)\right)$
36 35 adantr ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {G}\left(\mathrm{suc}{d}\right)={{F}}^{-1}\left({G}\left({d}\right)\right)$
37 1 2 3 4 infpssrlem1 ${⊢}{\phi }\to {G}\left(\varnothing \right)={C}$
38 37 adantl ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {G}\left(\varnothing \right)={C}$
39 34 36 38 3netr4d ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\varnothing \right)$
40 39 3adant3 ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\varnothing \right)$
41 5 neeq2d ${⊢}{c}=\varnothing \to \left({G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)↔{G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\varnothing \right)\right)$
42 40 41 syl5ibr ${⊢}{c}=\varnothing \to \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)$
43 42 adantrd ${⊢}{c}=\varnothing \to \left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)$
44 simpr ${⊢}\left({d}\in \mathrm{\omega }\wedge {c}\in \mathrm{suc}{d}\right)\to {c}\in \mathrm{suc}{d}$
45 peano2 ${⊢}{d}\in \mathrm{\omega }\to \mathrm{suc}{d}\in \mathrm{\omega }$
46 45 adantr ${⊢}\left({d}\in \mathrm{\omega }\wedge {c}\in \mathrm{suc}{d}\right)\to \mathrm{suc}{d}\in \mathrm{\omega }$
47 elnn ${⊢}\left({c}\in \mathrm{suc}{d}\wedge \mathrm{suc}{d}\in \mathrm{\omega }\right)\to {c}\in \mathrm{\omega }$
48 44 46 47 syl2anc ${⊢}\left({d}\in \mathrm{\omega }\wedge {c}\in \mathrm{suc}{d}\right)\to {c}\in \mathrm{\omega }$
49 48 3ad2antl1 ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to {c}\in \mathrm{\omega }$
50 49 adantl ${⊢}\left({c}\ne \varnothing \wedge \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\right)\to {c}\in \mathrm{\omega }$
51 simpl ${⊢}\left({c}\ne \varnothing \wedge \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\right)\to {c}\ne \varnothing$
52 nnsuc ${⊢}\left({c}\in \mathrm{\omega }\wedge {c}\ne \varnothing \right)\to \exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{c}=\mathrm{suc}{b}$
53 50 51 52 syl2anc ${⊢}\left({c}\ne \varnothing \wedge \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\right)\to \exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{c}=\mathrm{suc}{b}$
54 nfv ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}{d}\in \mathrm{\omega }$
55 nfv ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}{\phi }$
56 nfra1 ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)$
57 54 55 56 nf3an ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)$
58 nfv ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}{c}\in \mathrm{suc}{d}$
59 57 58 nfan ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)$
60 nfv ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)$
61 simpl3 ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)$
62 simpr ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to \mathrm{suc}{b}\in \mathrm{suc}{d}$
63 nnord ${⊢}{d}\in \mathrm{\omega }\to \mathrm{Ord}{d}$
64 63 adantr ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to \mathrm{Ord}{d}$
65 ordsucelsuc ${⊢}\mathrm{Ord}{d}\to \left({b}\in {d}↔\mathrm{suc}{b}\in \mathrm{suc}{d}\right)$
66 64 65 syl ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to \left({b}\in {d}↔\mathrm{suc}{b}\in \mathrm{suc}{d}\right)$
67 62 66 mpbird ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to {b}\in {d}$
68 67 3ad2antl1 ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to {b}\in {d}$
69 68 adantrr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to {b}\in {d}$
70 rsp ${⊢}\forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\to \left({b}\in {d}\to {G}\left({d}\right)\ne {G}\left({b}\right)\right)$
71 61 69 70 sylc ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to {G}\left({d}\right)\ne {G}\left({b}\right)$
72 f1of1 ${⊢}{{F}}^{-1}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{A}\underset{1-1}{⟶}{B}$
73 2 23 72 3syl ${⊢}{\phi }\to {{F}}^{-1}:{A}\underset{1-1}{⟶}{B}$
74 73 ad2antlr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to {{F}}^{-1}:{A}\underset{1-1}{⟶}{B}$
75 29 adantr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to {G}\left({d}\right)\in {A}$
76 27 ffvelrnda ${⊢}\left({\phi }\wedge {b}\in \mathrm{\omega }\right)\to {G}\left({b}\right)\in {A}$
77 76 adantll ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to {G}\left({b}\right)\in {A}$
78 f1fveq ${⊢}\left({{F}}^{-1}:{A}\underset{1-1}{⟶}{B}\wedge \left({G}\left({d}\right)\in {A}\wedge {G}\left({b}\right)\in {A}\right)\right)\to \left({{F}}^{-1}\left({G}\left({d}\right)\right)={{F}}^{-1}\left({G}\left({b}\right)\right)↔{G}\left({d}\right)={G}\left({b}\right)\right)$
79 74 75 77 78 syl12anc ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({{F}}^{-1}\left({G}\left({d}\right)\right)={{F}}^{-1}\left({G}\left({b}\right)\right)↔{G}\left({d}\right)={G}\left({b}\right)\right)$
80 79 necon3bid ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({{F}}^{-1}\left({G}\left({d}\right)\right)\ne {{F}}^{-1}\left({G}\left({b}\right)\right)↔{G}\left({d}\right)\ne {G}\left({b}\right)\right)$
81 80 biimprd ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({G}\left({d}\right)\ne {G}\left({b}\right)\to {{F}}^{-1}\left({G}\left({d}\right)\right)\ne {{F}}^{-1}\left({G}\left({b}\right)\right)\right)$
82 35 adantr ${⊢}\left({d}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to {G}\left(\mathrm{suc}{d}\right)={{F}}^{-1}\left({G}\left({d}\right)\right)$
83 1 2 3 4 infpssrlem2 ${⊢}{b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{b}\right)={{F}}^{-1}\left({G}\left({b}\right)\right)$
84 83 adantl ${⊢}\left({d}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to {G}\left(\mathrm{suc}{b}\right)={{F}}^{-1}\left({G}\left({b}\right)\right)$
85 82 84 neeq12d ${⊢}\left({d}\in \mathrm{\omega }\wedge {b}\in \mathrm{\omega }\right)\to \left({G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)↔{{F}}^{-1}\left({G}\left({d}\right)\right)\ne {{F}}^{-1}\left({G}\left({b}\right)\right)\right)$
86 85 adantlr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)↔{{F}}^{-1}\left({G}\left({d}\right)\right)\ne {{F}}^{-1}\left({G}\left({b}\right)\right)\right)$
87 81 86 sylibrd ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge {b}\in \mathrm{\omega }\right)\to \left({G}\left({d}\right)\ne {G}\left({b}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)$
88 87 adantrl ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to \left({G}\left({d}\right)\ne {G}\left({b}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)$
89 88 3adantl3 ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to \left({G}\left({d}\right)\ne {G}\left({b}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)$
90 71 89 mpd ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \left(\mathrm{suc}{b}\in \mathrm{suc}{d}\wedge {b}\in \mathrm{\omega }\right)\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)$
91 90 expr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to \left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)$
92 eleq1 ${⊢}{c}=\mathrm{suc}{b}\to \left({c}\in \mathrm{suc}{d}↔\mathrm{suc}{b}\in \mathrm{suc}{d}\right)$
93 92 anbi2d ${⊢}{c}=\mathrm{suc}{b}\to \left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)↔\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\right)$
94 fveq2 ${⊢}{c}=\mathrm{suc}{b}\to {G}\left({c}\right)={G}\left(\mathrm{suc}{b}\right)$
95 94 neeq2d ${⊢}{c}=\mathrm{suc}{b}\to \left({G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)↔{G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)$
96 95 imbi2d ${⊢}{c}=\mathrm{suc}{b}\to \left(\left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)↔\left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)\right)$
97 93 96 imbi12d ${⊢}{c}=\mathrm{suc}{b}\to \left(\left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to \left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)\right)↔\left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge \mathrm{suc}{b}\in \mathrm{suc}{d}\right)\to \left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left(\mathrm{suc}{b}\right)\right)\right)\right)$
98 91 97 mpbiri ${⊢}{c}=\mathrm{suc}{b}\to \left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to \left({b}\in \mathrm{\omega }\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)\right)$
99 98 com3l ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to \left({b}\in \mathrm{\omega }\to \left({c}=\mathrm{suc}{b}\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)\right)$
100 59 60 99 rexlimd ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to \left(\exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{c}=\mathrm{suc}{b}\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)$
101 100 adantl ${⊢}\left({c}\ne \varnothing \wedge \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\right)\to \left(\exists {b}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{c}=\mathrm{suc}{b}\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)$
102 53 101 mpd ${⊢}\left({c}\ne \varnothing \wedge \left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)$
103 102 ex ${⊢}{c}\ne \varnothing \to \left(\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)\right)$
104 43 103 pm2.61ine ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\wedge {c}\in \mathrm{suc}{d}\right)\to {G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)$
105 104 ralrimiva ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\to \forall {c}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)$
106 fveq2 ${⊢}{c}={b}\to {G}\left({c}\right)={G}\left({b}\right)$
107 106 neeq2d ${⊢}{c}={b}\to \left({G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)↔{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)$
108 107 cbvralvw ${⊢}\forall {c}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({c}\right)↔\forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)$
109 105 108 sylib ${⊢}\left({d}\in \mathrm{\omega }\wedge {\phi }\wedge \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\to \forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)$
110 109 3exp ${⊢}{d}\in \mathrm{\omega }\to \left({\phi }\to \left(\forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\to \forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)\right)$
111 110 a2d ${⊢}{d}\in \mathrm{\omega }\to \left(\left({\phi }\to \forall {b}\in {d}\phantom{\rule{.4em}{0ex}}{G}\left({d}\right)\ne {G}\left({b}\right)\right)\to \left({\phi }\to \forall {b}\in \mathrm{suc}{d}\phantom{\rule{.4em}{0ex}}{G}\left(\mathrm{suc}{d}\right)\ne {G}\left({b}\right)\right)\right)$
112 8 12 16 20 22 111 finds ${⊢}{M}\in \mathrm{\omega }\to \left({\phi }\to \forall {b}\in {M}\phantom{\rule{.4em}{0ex}}{G}\left({M}\right)\ne {G}\left({b}\right)\right)$
113 112 impcom ${⊢}\left({\phi }\wedge {M}\in \mathrm{\omega }\right)\to \forall {b}\in {M}\phantom{\rule{.4em}{0ex}}{G}\left({M}\right)\ne {G}\left({b}\right)$
114 fveq2 ${⊢}{b}={N}\to {G}\left({b}\right)={G}\left({N}\right)$
115 114 neeq2d ${⊢}{b}={N}\to \left({G}\left({M}\right)\ne {G}\left({b}\right)↔{G}\left({M}\right)\ne {G}\left({N}\right)\right)$
116 115 rspccv ${⊢}\forall {b}\in {M}\phantom{\rule{.4em}{0ex}}{G}\left({M}\right)\ne {G}\left({b}\right)\to \left({N}\in {M}\to {G}\left({M}\right)\ne {G}\left({N}\right)\right)$
117 113 116 syl ${⊢}\left({\phi }\wedge {M}\in \mathrm{\omega }\right)\to \left({N}\in {M}\to {G}\left({M}\right)\ne {G}\left({N}\right)\right)$
118 117 3impia ${⊢}\left({\phi }\wedge {M}\in \mathrm{\omega }\wedge {N}\in {M}\right)\to {G}\left({M}\right)\ne {G}\left({N}\right)$