# Metamath Proof Explorer

## Theorem ttukeylem5

Description: Lemma for ttukey . The G function forms a (transfinitely long) chain of inclusions. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 ${⊢}{\phi }\to {F}:\mathrm{card}\left(\bigcup {A}\setminus {B}\right)\underset{1-1 onto}{⟶}\bigcup {A}\setminus {B}$
ttukeylem.2 ${⊢}{\phi }\to {B}\in {A}$
ttukeylem.3 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔𝒫{x}\cap \mathrm{Fin}\subseteq {A}\right)$
ttukeylem.4 ${⊢}{G}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼if\left(\mathrm{dom}{z}=\bigcup \mathrm{dom}{z},if\left(\mathrm{dom}{z}=\varnothing ,{B},\bigcup \mathrm{ran}{z}\right),{z}\left(\bigcup \mathrm{dom}{z}\right)\cup if\left({z}\left(\bigcup \mathrm{dom}{z}\right)\cup \left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\}\in {A},\left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\},\varnothing \right)\right)\right)\right)$
Assertion ttukeylem5 ${⊢}\left({\phi }\wedge \left({C}\in \mathrm{On}\wedge {D}\in \mathrm{On}\wedge {C}\subseteq {D}\right)\right)\to {G}\left({C}\right)\subseteq {G}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 ttukeylem.1 ${⊢}{\phi }\to {F}:\mathrm{card}\left(\bigcup {A}\setminus {B}\right)\underset{1-1 onto}{⟶}\bigcup {A}\setminus {B}$
2 ttukeylem.2 ${⊢}{\phi }\to {B}\in {A}$
3 ttukeylem.3 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔𝒫{x}\cap \mathrm{Fin}\subseteq {A}\right)$
4 ttukeylem.4 ${⊢}{G}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼if\left(\mathrm{dom}{z}=\bigcup \mathrm{dom}{z},if\left(\mathrm{dom}{z}=\varnothing ,{B},\bigcup \mathrm{ran}{z}\right),{z}\left(\bigcup \mathrm{dom}{z}\right)\cup if\left({z}\left(\bigcup \mathrm{dom}{z}\right)\cup \left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\}\in {A},\left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\},\varnothing \right)\right)\right)\right)$
5 sseq2 ${⊢}{y}={a}\to \left({C}\subseteq {y}↔{C}\subseteq {a}\right)$
6 fveq2 ${⊢}{y}={a}\to {G}\left({y}\right)={G}\left({a}\right)$
7 6 sseq2d ${⊢}{y}={a}\to \left({G}\left({C}\right)\subseteq {G}\left({y}\right)↔{G}\left({C}\right)\subseteq {G}\left({a}\right)\right)$
8 5 7 imbi12d ${⊢}{y}={a}\to \left(\left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)↔\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)$
9 8 imbi2d ${⊢}{y}={a}\to \left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)↔\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\right)$
10 sseq2 ${⊢}{y}={D}\to \left({C}\subseteq {y}↔{C}\subseteq {D}\right)$
11 fveq2 ${⊢}{y}={D}\to {G}\left({y}\right)={G}\left({D}\right)$
12 11 sseq2d ${⊢}{y}={D}\to \left({G}\left({C}\right)\subseteq {G}\left({y}\right)↔{G}\left({C}\right)\subseteq {G}\left({D}\right)\right)$
13 10 12 imbi12d ${⊢}{y}={D}\to \left(\left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)↔\left({C}\subseteq {D}\to {G}\left({C}\right)\subseteq {G}\left({D}\right)\right)\right)$
14 13 imbi2d ${⊢}{y}={D}\to \left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)↔\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {D}\to {G}\left({C}\right)\subseteq {G}\left({D}\right)\right)\right)\right)$
15 r19.21v ${⊢}\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)↔\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)$
16 onsseleq ${⊢}\left({C}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({C}\subseteq {y}↔\left({C}\in {y}\vee {C}={y}\right)\right)$
17 16 ad4ant23 ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left({C}\subseteq {y}↔\left({C}\in {y}\vee {C}={y}\right)\right)$
18 sseq2 ${⊢}if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)=if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)\to \left({G}\left({C}\right)\subseteq if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)↔{G}\left({C}\right)\subseteq if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)\right)$
19 sseq2 ${⊢}{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)=if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)\to \left({G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)↔{G}\left({C}\right)\subseteq if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)\right)$
20 4 tfr1 ${⊢}{G}Fn\mathrm{On}$
21 simplr ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {y}\in \mathrm{On}$
22 onss ${⊢}{y}\in \mathrm{On}\to {y}\subseteq \mathrm{On}$
23 21 22 syl ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {y}\subseteq \mathrm{On}$
24 simprr ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {C}\in {y}$
25 fnfvima ${⊢}\left({G}Fn\mathrm{On}\wedge {y}\subseteq \mathrm{On}\wedge {C}\in {y}\right)\to {G}\left({C}\right)\in {G}\left[{y}\right]$
26 20 23 24 25 mp3an2i ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({C}\right)\in {G}\left[{y}\right]$
27 elssuni ${⊢}{G}\left({C}\right)\in {G}\left[{y}\right]\to {G}\left({C}\right)\subseteq \bigcup {G}\left[{y}\right]$
28 26 27 syl ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({C}\right)\subseteq \bigcup {G}\left[{y}\right]$
29 n0i ${⊢}{C}\in {y}\to ¬{y}=\varnothing$
30 iffalse ${⊢}¬{y}=\varnothing \to if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)=\bigcup {G}\left[{y}\right]$
31 24 29 30 3syl ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)=\bigcup {G}\left[{y}\right]$
32 28 31 sseqtrrd ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({C}\right)\subseteq if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)$
33 32 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge {y}=\bigcup {y}\right)\to {G}\left({C}\right)\subseteq if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right)$
34 24 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to {C}\in {y}$
35 elssuni ${⊢}{C}\in {y}\to {C}\subseteq \bigcup {y}$
36 34 35 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to {C}\subseteq \bigcup {y}$
37 sseq2 ${⊢}{a}=\bigcup {y}\to \left({C}\subseteq {a}↔{C}\subseteq \bigcup {y}\right)$
38 fveq2 ${⊢}{a}=\bigcup {y}\to {G}\left({a}\right)={G}\left(\bigcup {y}\right)$
39 38 sseq2d ${⊢}{a}=\bigcup {y}\to \left({G}\left({C}\right)\subseteq {G}\left({a}\right)↔{G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)\right)$
40 37 39 imbi12d ${⊢}{a}=\bigcup {y}\to \left(\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)↔\left({C}\subseteq \bigcup {y}\to {G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)\right)\right)$
41 simplrl ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)$
42 vuniex ${⊢}\bigcup {y}\in \mathrm{V}$
43 42 sucid ${⊢}\bigcup {y}\in \mathrm{suc}\bigcup {y}$
44 eloni ${⊢}{y}\in \mathrm{On}\to \mathrm{Ord}{y}$
45 orduniorsuc ${⊢}\mathrm{Ord}{y}\to \left({y}=\bigcup {y}\vee {y}=\mathrm{suc}\bigcup {y}\right)$
46 21 44 45 3syl ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to \left({y}=\bigcup {y}\vee {y}=\mathrm{suc}\bigcup {y}\right)$
47 46 orcanai ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to {y}=\mathrm{suc}\bigcup {y}$
48 43 47 eleqtrrid ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to \bigcup {y}\in {y}$
49 40 41 48 rspcdva ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to \left({C}\subseteq \bigcup {y}\to {G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)\right)$
50 36 49 mpd ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to {G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)$
51 ssun1 ${⊢}{G}\left(\bigcup {y}\right)\subseteq {G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)$
52 50 51 sstrdi ${⊢}\left(\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\wedge ¬{y}=\bigcup {y}\right)\to {G}\left({C}\right)\subseteq {G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)$
53 18 19 33 52 ifbothda ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({C}\right)\subseteq if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)$
54 1 2 3 4 ttukeylem3 ${⊢}\left({\phi }\wedge {y}\in \mathrm{On}\right)\to {G}\left({y}\right)=if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)$
55 54 ad4ant13 ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({y}\right)=if\left({y}=\bigcup {y},if\left({y}=\varnothing ,{B},\bigcup {G}\left[{y}\right]\right),{G}\left(\bigcup {y}\right)\cup if\left({G}\left(\bigcup {y}\right)\cup \left\{{F}\left(\bigcup {y}\right)\right\}\in {A},\left\{{F}\left(\bigcup {y}\right)\right\},\varnothing \right)\right)$
56 53 55 sseqtrrd ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\wedge {C}\in {y}\right)\right)\to {G}\left({C}\right)\subseteq {G}\left({y}\right)$
57 56 expr ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left({C}\in {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)$
58 fveq2 ${⊢}{C}={y}\to {G}\left({C}\right)={G}\left({y}\right)$
59 eqimss ${⊢}{G}\left({C}\right)={G}\left({y}\right)\to {G}\left({C}\right)\subseteq {G}\left({y}\right)$
60 58 59 syl ${⊢}{C}={y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)$
61 60 a1i ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left({C}={y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)$
62 57 61 jaod ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left(\left({C}\in {y}\vee {C}={y}\right)\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)$
63 17 62 sylbid ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\wedge \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)$
64 63 ex ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {y}\in \mathrm{On}\right)\to \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)$
65 64 expcom ${⊢}{y}\in \mathrm{On}\to \left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)\right)$
66 65 a2d ${⊢}{y}\in \mathrm{On}\to \left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)\right)$
67 15 66 syl5bi ${⊢}{y}\in \mathrm{On}\to \left(\forall {a}\in {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {a}\to {G}\left({C}\right)\subseteq {G}\left({a}\right)\right)\right)\to \left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {y}\to {G}\left({C}\right)\subseteq {G}\left({y}\right)\right)\right)\right)$
68 9 14 67 tfis3 ${⊢}{D}\in \mathrm{On}\to \left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \left({C}\subseteq {D}\to {G}\left({C}\right)\subseteq {G}\left({D}\right)\right)\right)$
69 68 expdcom ${⊢}{\phi }\to \left({C}\in \mathrm{On}\to \left({D}\in \mathrm{On}\to \left({C}\subseteq {D}\to {G}\left({C}\right)\subseteq {G}\left({D}\right)\right)\right)\right)$
70 69 3imp2 ${⊢}\left({\phi }\wedge \left({C}\in \mathrm{On}\wedge {D}\in \mathrm{On}\wedge {C}\subseteq {D}\right)\right)\to {G}\left({C}\right)\subseteq {G}\left({D}\right)$