# Metamath Proof Explorer

## Theorem isf32lem2

Description: Lemma for isfin3-2 . Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
Assertion isf32lem2 ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)$

### Proof

Step Hyp Ref Expression
1 isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
2 isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
3 isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
4 3 adantr ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
5 1 ffnd ${⊢}{\phi }\to {F}Fn\mathrm{\omega }$
6 peano2 ${⊢}{A}\in \mathrm{\omega }\to \mathrm{suc}{A}\in \mathrm{\omega }$
7 fnfvelrn ${⊢}\left({F}Fn\mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\to {F}\left(\mathrm{suc}{A}\right)\in \mathrm{ran}{F}$
8 5 6 7 syl2an ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {F}\left(\mathrm{suc}{A}\right)\in \mathrm{ran}{F}$
9 8 adantr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to {F}\left(\mathrm{suc}{A}\right)\in \mathrm{ran}{F}$
10 intss1 ${⊢}{F}\left(\mathrm{suc}{A}\right)\in \mathrm{ran}{F}\to \bigcap \mathrm{ran}{F}\subseteq {F}\left(\mathrm{suc}{A}\right)$
11 9 10 syl ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \bigcap \mathrm{ran}{F}\subseteq {F}\left(\mathrm{suc}{A}\right)$
12 fvelrnb ${⊢}{F}Fn\mathrm{\omega }\to \left({b}\in \mathrm{ran}{F}↔\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)={b}\right)$
13 5 12 syl ${⊢}{\phi }\to \left({b}\in \mathrm{ran}{F}↔\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)={b}\right)$
14 13 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \left({b}\in \mathrm{ran}{F}↔\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)={b}\right)$
15 simplrr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to {c}\in \mathrm{\omega }$
16 6 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to \mathrm{suc}{A}\in \mathrm{\omega }$
17 simpr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to \mathrm{suc}{A}\subseteq {c}$
18 simplrl ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
19 fveq2 ${⊢}{b}=\mathrm{suc}{A}\to {F}\left({b}\right)={F}\left(\mathrm{suc}{A}\right)$
20 19 eqeq2d ${⊢}{b}=\mathrm{suc}{A}\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)↔{F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{A}\right)\right)$
21 20 imbi2d ${⊢}{b}=\mathrm{suc}{A}\to \left(\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)\right)↔\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{A}\right)\right)\right)$
22 fveq2 ${⊢}{b}={d}\to {F}\left({b}\right)={F}\left({d}\right)$
23 22 eqeq2d ${⊢}{b}={d}\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)↔{F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\right)$
24 23 imbi2d ${⊢}{b}={d}\to \left(\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)\right)↔\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\right)\right)$
25 fveq2 ${⊢}{b}=\mathrm{suc}{d}\to {F}\left({b}\right)={F}\left(\mathrm{suc}{d}\right)$
26 25 eqeq2d ${⊢}{b}=\mathrm{suc}{d}\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)↔{F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)\right)$
27 26 imbi2d ${⊢}{b}=\mathrm{suc}{d}\to \left(\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)\right)↔\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)\right)\right)$
28 fveq2 ${⊢}{b}={c}\to {F}\left({b}\right)={F}\left({c}\right)$
29 28 eqeq2d ${⊢}{b}={c}\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)↔{F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)\right)$
30 29 imbi2d ${⊢}{b}={c}\to \left(\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({b}\right)\right)↔\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)\right)\right)$
31 eqid ${⊢}{F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{A}\right)$
32 31 2a1i ${⊢}\mathrm{suc}{A}\in \mathrm{\omega }\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{A}\right)\right)$
33 elex ${⊢}\mathrm{suc}{A}\in \mathrm{\omega }\to \mathrm{suc}{A}\in \mathrm{V}$
34 sucexb ${⊢}{A}\in \mathrm{V}↔\mathrm{suc}{A}\in \mathrm{V}$
35 33 34 sylibr ${⊢}\mathrm{suc}{A}\in \mathrm{\omega }\to {A}\in \mathrm{V}$
36 35 adantl ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\to {A}\in \mathrm{V}$
37 sucssel ${⊢}{A}\in \mathrm{V}\to \left(\mathrm{suc}{A}\subseteq {d}\to {A}\in {d}\right)$
38 36 37 syl ${⊢}\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\to \left(\mathrm{suc}{A}\subseteq {d}\to {A}\in {d}\right)$
39 38 imp ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {d}\right)\to {A}\in {d}$
40 eleq2w ${⊢}{a}={d}\to \left({A}\in {a}↔{A}\in {d}\right)$
41 suceq ${⊢}{a}={d}\to \mathrm{suc}{a}=\mathrm{suc}{d}$
42 41 fveq2d ${⊢}{a}={d}\to {F}\left(\mathrm{suc}{a}\right)={F}\left(\mathrm{suc}{d}\right)$
43 fveq2 ${⊢}{a}={d}\to {F}\left({a}\right)={F}\left({d}\right)$
44 42 43 eqeq12d ${⊢}{a}={d}\to \left({F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)↔{F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)$
45 40 44 imbi12d ${⊢}{a}={d}\to \left(\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)↔\left({A}\in {d}\to {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)\right)$
46 45 rspcv ${⊢}{d}\in \mathrm{\omega }\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({A}\in {d}\to {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)\right)$
47 46 com23 ${⊢}{d}\in \mathrm{\omega }\to \left({A}\in {d}\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)\right)$
48 47 ad2antrr ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {d}\right)\to \left({A}\in {d}\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)\right)$
49 39 48 mpd ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {d}\right)\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)$
50 eqtr3 ${⊢}\left({F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\wedge {F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)$
51 50 expcom ${⊢}{F}\left(\mathrm{suc}{d}\right)={F}\left({d}\right)\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)\right)$
52 49 51 syl6 ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {d}\right)\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)\right)\right)$
53 52 a2d ${⊢}\left(\left({d}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {d}\right)\to \left(\left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({d}\right)\right)\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left(\mathrm{suc}{d}\right)\right)\right)$
54 21 24 27 30 32 53 findsg ${⊢}\left(\left({c}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)\right)$
55 54 impr ${⊢}\left(\left({c}\in \mathrm{\omega }\wedge \mathrm{suc}{A}\in \mathrm{\omega }\right)\wedge \left(\mathrm{suc}{A}\subseteq {c}\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)$
56 15 16 17 18 55 syl22anc ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to {F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)$
57 eqimss ${⊢}{F}\left(\mathrm{suc}{A}\right)={F}\left({c}\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
58 56 57 syl ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge \mathrm{suc}{A}\subseteq {c}\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
59 6 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge {c}\subseteq \mathrm{suc}{A}\right)\to \mathrm{suc}{A}\in \mathrm{\omega }$
60 simplrr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge {c}\subseteq \mathrm{suc}{A}\right)\to {c}\in \mathrm{\omega }$
61 simpr ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge {c}\subseteq \mathrm{suc}{A}\right)\to {c}\subseteq \mathrm{suc}{A}$
62 simplll ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge {c}\subseteq \mathrm{suc}{A}\right)\to {\phi }$
63 1 2 3 isf32lem1 ${⊢}\left(\left(\mathrm{suc}{A}\in \mathrm{\omega }\wedge {c}\in \mathrm{\omega }\right)\wedge \left({c}\subseteq \mathrm{suc}{A}\wedge {\phi }\right)\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
64 59 60 61 62 63 syl22anc ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\wedge {c}\subseteq \mathrm{suc}{A}\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
65 nnord ${⊢}\mathrm{suc}{A}\in \mathrm{\omega }\to \mathrm{Ord}\mathrm{suc}{A}$
66 6 65 syl ${⊢}{A}\in \mathrm{\omega }\to \mathrm{Ord}\mathrm{suc}{A}$
67 66 ad2antlr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\to \mathrm{Ord}\mathrm{suc}{A}$
68 nnord ${⊢}{c}\in \mathrm{\omega }\to \mathrm{Ord}{c}$
69 68 ad2antll ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\to \mathrm{Ord}{c}$
70 ordtri2or2 ${⊢}\left(\mathrm{Ord}\mathrm{suc}{A}\wedge \mathrm{Ord}{c}\right)\to \left(\mathrm{suc}{A}\subseteq {c}\vee {c}\subseteq \mathrm{suc}{A}\right)$
71 67 69 70 syl2anc ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\to \left(\mathrm{suc}{A}\subseteq {c}\vee {c}\subseteq \mathrm{suc}{A}\right)$
72 58 64 71 mpjaodan ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \left(\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\wedge {c}\in \mathrm{\omega }\right)\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
73 72 anassrs ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\wedge {c}\in \mathrm{\omega }\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)$
74 sseq2 ${⊢}{F}\left({c}\right)={b}\to \left({F}\left(\mathrm{suc}{A}\right)\subseteq {F}\left({c}\right)↔{F}\left(\mathrm{suc}{A}\right)\subseteq {b}\right)$
75 73 74 syl5ibcom ${⊢}\left(\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\wedge {c}\in \mathrm{\omega }\right)\to \left({F}\left({c}\right)={b}\to {F}\left(\mathrm{suc}{A}\right)\subseteq {b}\right)$
76 75 rexlimdva ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \left(\exists {c}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left({c}\right)={b}\to {F}\left(\mathrm{suc}{A}\right)\subseteq {b}\right)$
77 14 76 sylbid ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \left({b}\in \mathrm{ran}{F}\to {F}\left(\mathrm{suc}{A}\right)\subseteq {b}\right)$
78 77 ralrimiv ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \forall {b}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{A}\right)\subseteq {b}$
79 ssint ${⊢}{F}\left(\mathrm{suc}{A}\right)\subseteq \bigcap \mathrm{ran}{F}↔\forall {b}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{A}\right)\subseteq {b}$
80 78 79 sylibr ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to {F}\left(\mathrm{suc}{A}\right)\subseteq \bigcap \mathrm{ran}{F}$
81 11 80 eqssd ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \bigcap \mathrm{ran}{F}={F}\left(\mathrm{suc}{A}\right)$
82 81 9 eqeltrd ${⊢}\left(\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\wedge \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\right)\to \bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
83 4 82 mtand ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to ¬\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
84 rexnal ${⊢}\exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)↔¬\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
85 83 84 sylibr ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
86 suceq ${⊢}{x}={a}\to \mathrm{suc}{x}=\mathrm{suc}{a}$
87 86 fveq2d ${⊢}{x}={a}\to {F}\left(\mathrm{suc}{x}\right)={F}\left(\mathrm{suc}{a}\right)$
88 fveq2 ${⊢}{x}={a}\to {F}\left({x}\right)={F}\left({a}\right)$
89 87 88 sseq12d ${⊢}{x}={a}\to \left({F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)↔{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\right)$
90 89 cbvralvw ${⊢}\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)↔\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)$
91 2 90 sylib ${⊢}{\phi }\to \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)$
92 91 adantr ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)$
93 pm4.61 ${⊢}¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)↔\left({A}\in {a}\wedge ¬{F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
94 dfpss2 ${⊢}{F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)↔\left({F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\wedge ¬{F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)$
95 94 simplbi2 ${⊢}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\to \left(¬{F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\to {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)$
96 95 anim2d ${⊢}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\to \left(\left({A}\in {a}\wedge ¬{F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)$
97 93 96 syl5bi ${⊢}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\to \left(¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)$
98 97 ralimi ${⊢}\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{a}\right)\subseteq {F}\left({a}\right)\to \forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)$
99 rexim ${⊢}\forall {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left(¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)\to \left(\exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)$
100 92 98 99 3syl ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left(\exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}¬\left({A}\in {a}\to {F}\left(\mathrm{suc}{a}\right)={F}\left({a}\right)\right)\to \exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)\right)$
101 85 100 mpd ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \exists {a}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({A}\in {a}\wedge {F}\left(\mathrm{suc}{a}\right)\subset {F}\left({a}\right)\right)$