# Metamath Proof Explorer

## Theorem fin23lem34

Description: Lemma for fin23 . Establish induction invariants on Y which parameterizes our contradictory chain of subsets. In this section, h is the hypothetically assumed family of subsets, g is the ground set, and i is the induction function constructed in the previous section. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ${⊢}{F}=\left\{{g}|\forall {a}\in \left({𝒫{g}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}\left(\mathrm{suc}{x}\right)\subseteq {a}\left({x}\right)\to \bigcap \mathrm{ran}{a}\in \mathrm{ran}{a}\right)\right\}$
fin23lem.f ${⊢}{\phi }\to {h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$
fin23lem.g ${⊢}{\phi }\to \bigcup \mathrm{ran}{h}\subseteq {G}$
fin23lem.h ${⊢}{\phi }\to \forall {j}\phantom{\rule{.4em}{0ex}}\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)$
fin23lem.i ${⊢}{Y}={\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}$
Assertion fin23lem34 ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left({Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)$

### Proof

Step Hyp Ref Expression
1 fin23lem33.f ${⊢}{F}=\left\{{g}|\forall {a}\in \left({𝒫{g}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}\left(\mathrm{suc}{x}\right)\subseteq {a}\left({x}\right)\to \bigcap \mathrm{ran}{a}\in \mathrm{ran}{a}\right)\right\}$
2 fin23lem.f ${⊢}{\phi }\to {h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$
3 fin23lem.g ${⊢}{\phi }\to \bigcup \mathrm{ran}{h}\subseteq {G}$
4 fin23lem.h ${⊢}{\phi }\to \forall {j}\phantom{\rule{.4em}{0ex}}\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)$
5 fin23lem.i ${⊢}{Y}={\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}$
6 fveq2 ${⊢}{a}=\varnothing \to {Y}\left({a}\right)={Y}\left(\varnothing \right)$
7 f1eq1 ${⊢}{Y}\left({a}\right)={Y}\left(\varnothing \right)\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
8 6 7 syl ${⊢}{a}=\varnothing \to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
9 6 rneqd ${⊢}{a}=\varnothing \to \mathrm{ran}{Y}\left({a}\right)=\mathrm{ran}{Y}\left(\varnothing \right)$
10 9 unieqd ${⊢}{a}=\varnothing \to \bigcup \mathrm{ran}{Y}\left({a}\right)=\bigcup \mathrm{ran}{Y}\left(\varnothing \right)$
11 10 sseq1d ${⊢}{a}=\varnothing \to \left(\bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}↔\bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}\right)$
12 8 11 anbi12d ${⊢}{a}=\varnothing \to \left(\left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)↔\left({Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}\right)\right)$
13 12 imbi2d ${⊢}{a}=\varnothing \to \left(\left({\phi }\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)\right)↔\left({\phi }\to \left({Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}\right)\right)\right)$
14 fveq2 ${⊢}{a}={b}\to {Y}\left({a}\right)={Y}\left({b}\right)$
15 f1eq1 ${⊢}{Y}\left({a}\right)={Y}\left({b}\right)\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
16 14 15 syl ${⊢}{a}={b}\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
17 14 rneqd ${⊢}{a}={b}\to \mathrm{ran}{Y}\left({a}\right)=\mathrm{ran}{Y}\left({b}\right)$
18 17 unieqd ${⊢}{a}={b}\to \bigcup \mathrm{ran}{Y}\left({a}\right)=\bigcup \mathrm{ran}{Y}\left({b}\right)$
19 18 sseq1d ${⊢}{a}={b}\to \left(\bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}↔\bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)$
20 16 19 anbi12d ${⊢}{a}={b}\to \left(\left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)↔\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)$
21 20 imbi2d ${⊢}{a}={b}\to \left(\left({\phi }\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)\right)↔\left({\phi }\to \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\right)$
22 fveq2 ${⊢}{a}=\mathrm{suc}{b}\to {Y}\left({a}\right)={Y}\left(\mathrm{suc}{b}\right)$
23 f1eq1 ${⊢}{Y}\left({a}\right)={Y}\left(\mathrm{suc}{b}\right)\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
24 22 23 syl ${⊢}{a}=\mathrm{suc}{b}\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
25 22 rneqd ${⊢}{a}=\mathrm{suc}{b}\to \mathrm{ran}{Y}\left({a}\right)=\mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)$
26 25 unieqd ${⊢}{a}=\mathrm{suc}{b}\to \bigcup \mathrm{ran}{Y}\left({a}\right)=\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)$
27 26 sseq1d ${⊢}{a}=\mathrm{suc}{b}\to \left(\bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}↔\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)$
28 24 27 anbi12d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)↔\left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)\right)$
29 28 imbi2d ${⊢}{a}=\mathrm{suc}{b}\to \left(\left({\phi }\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)\right)↔\left({\phi }\to \left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)\right)\right)$
30 fveq2 ${⊢}{a}={A}\to {Y}\left({a}\right)={Y}\left({A}\right)$
31 f1eq1 ${⊢}{Y}\left({a}\right)={Y}\left({A}\right)\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
32 30 31 syl ${⊢}{a}={A}\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
33 30 rneqd ${⊢}{a}={A}\to \mathrm{ran}{Y}\left({a}\right)=\mathrm{ran}{Y}\left({A}\right)$
34 33 unieqd ${⊢}{a}={A}\to \bigcup \mathrm{ran}{Y}\left({a}\right)=\bigcup \mathrm{ran}{Y}\left({A}\right)$
35 34 sseq1d ${⊢}{a}={A}\to \left(\bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}↔\bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)$
36 32 35 anbi12d ${⊢}{a}={A}\to \left(\left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)↔\left({Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)\right)$
37 36 imbi2d ${⊢}{a}={A}\to \left(\left({\phi }\to \left({Y}\left({a}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({a}\right)\subseteq {G}\right)\right)↔\left({\phi }\to \left({Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)\right)\right)$
38 5 fveq1i ${⊢}{Y}\left(\varnothing \right)=\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)$
39 fr0g ${⊢}{h}\in \mathrm{V}\to \left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)={h}$
40 39 elv ${⊢}\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left(\varnothing \right)={h}$
41 38 40 eqtri ${⊢}{Y}\left(\varnothing \right)={h}$
42 f1eq1 ${⊢}{Y}\left(\varnothing \right)={h}\to \left({Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
43 41 42 ax-mp ${⊢}{Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$
44 41 rneqi ${⊢}\mathrm{ran}{Y}\left(\varnothing \right)=\mathrm{ran}{h}$
45 44 unieqi ${⊢}\bigcup \mathrm{ran}{Y}\left(\varnothing \right)=\bigcup \mathrm{ran}{h}$
46 45 sseq1i ${⊢}\bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}↔\bigcup \mathrm{ran}{h}\subseteq {G}$
47 43 46 anbi12i ${⊢}\left({Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}\right)↔\left({h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{h}\subseteq {G}\right)$
48 2 3 47 sylanbrc ${⊢}{\phi }\to \left({Y}\left(\varnothing \right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\varnothing \right)\subseteq {G}\right)$
49 fvex ${⊢}{Y}\left({b}\right)\in \mathrm{V}$
50 f1eq1 ${⊢}{j}={Y}\left({b}\right)\to \left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
51 rneq ${⊢}{j}={Y}\left({b}\right)\to \mathrm{ran}{j}=\mathrm{ran}{Y}\left({b}\right)$
52 51 unieqd ${⊢}{j}={Y}\left({b}\right)\to \bigcup \mathrm{ran}{j}=\bigcup \mathrm{ran}{Y}\left({b}\right)$
53 52 sseq1d ${⊢}{j}={Y}\left({b}\right)\to \left(\bigcup \mathrm{ran}{j}\subseteq {G}↔\bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)$
54 50 53 anbi12d ${⊢}{j}={Y}\left({b}\right)\to \left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)↔\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)$
55 fveq2 ${⊢}{j}={Y}\left({b}\right)\to {i}\left({j}\right)={i}\left({Y}\left({b}\right)\right)$
56 f1eq1 ${⊢}{i}\left({j}\right)={i}\left({Y}\left({b}\right)\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
57 55 56 syl ${⊢}{j}={Y}\left({b}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
58 55 rneqd ${⊢}{j}={Y}\left({b}\right)\to \mathrm{ran}{i}\left({j}\right)=\mathrm{ran}{i}\left({Y}\left({b}\right)\right)$
59 58 unieqd ${⊢}{j}={Y}\left({b}\right)\to \bigcup \mathrm{ran}{i}\left({j}\right)=\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)$
60 59 52 psseq12d ${⊢}{j}={Y}\left({b}\right)\to \left(\bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}↔\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)$
61 57 60 anbi12d ${⊢}{j}={Y}\left({b}\right)\to \left(\left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)↔\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\right)$
62 54 61 imbi12d ${⊢}{j}={Y}\left({b}\right)\to \left(\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)↔\left(\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\right)\right)$
63 49 62 spcv ${⊢}\forall {j}\phantom{\rule{.4em}{0ex}}\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)\to \left(\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\right)$
64 4 63 syl ${⊢}{\phi }\to \left(\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\right)$
65 64 imp ${⊢}\left({\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)$
66 pssss ${⊢}\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\to \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq \bigcup \mathrm{ran}{Y}\left({b}\right)$
67 sstr ${⊢}\left(\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq \bigcup \mathrm{ran}{Y}\left({b}\right)\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}$
68 66 67 sylan ${⊢}\left(\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}$
69 68 expcom ${⊢}\bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\to \left(\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\to \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)$
70 69 anim2d ${⊢}\bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\to \left(\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)\right)$
71 70 ad2antll ${⊢}\left({\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left(\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subset \bigcup \mathrm{ran}{Y}\left({b}\right)\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)\right)$
72 65 71 mpd ${⊢}\left({\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)$
73 72 3adant1 ${⊢}\left({b}\in \mathrm{\omega }\wedge {\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)$
74 frsuc ${⊢}{b}\in \mathrm{\omega }\to \left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{b}\right)={i}\left(\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left({b}\right)\right)$
75 5 fveq1i ${⊢}{Y}\left(\mathrm{suc}{b}\right)=\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{b}\right)$
76 5 fveq1i ${⊢}{Y}\left({b}\right)=\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left({b}\right)$
77 76 fveq2i ${⊢}{i}\left({Y}\left({b}\right)\right)={i}\left(\left({\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}\right)\left({b}\right)\right)$
78 74 75 77 3eqtr4g ${⊢}{b}\in \mathrm{\omega }\to {Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)$
79 f1eq1 ${⊢}{Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)\to \left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}↔{i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$
80 rneq ${⊢}{Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)\to \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)=\mathrm{ran}{i}\left({Y}\left({b}\right)\right)$
81 80 unieqd ${⊢}{Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)\to \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)=\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)$
82 81 sseq1d ${⊢}{Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)\to \left(\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}↔\bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)$
83 79 82 anbi12d ${⊢}{Y}\left(\mathrm{suc}{b}\right)={i}\left({Y}\left({b}\right)\right)\to \left(\left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)↔\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)\right)$
84 78 83 syl ${⊢}{b}\in \mathrm{\omega }\to \left(\left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)↔\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)\right)$
85 84 3ad2ant1 ${⊢}\left({b}\in \mathrm{\omega }\wedge {\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left(\left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)↔\left({i}\left({Y}\left({b}\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({Y}\left({b}\right)\right)\subseteq {G}\right)\right)$
86 73 85 mpbird ${⊢}\left({b}\in \mathrm{\omega }\wedge {\phi }\wedge \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)$
87 86 3exp ${⊢}{b}\in \mathrm{\omega }\to \left({\phi }\to \left(\left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\to \left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)\right)\right)$
88 87 a2d ${⊢}{b}\in \mathrm{\omega }\to \left(\left({\phi }\to \left({Y}\left({b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({b}\right)\subseteq {G}\right)\right)\to \left({\phi }\to \left({Y}\left(\mathrm{suc}{b}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{b}\right)\subseteq {G}\right)\right)\right)$
89 13 21 29 37 48 88 finds ${⊢}{A}\in \mathrm{\omega }\to \left({\phi }\to \left({Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)\right)$
90 89 impcom ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left({Y}\left({A}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({A}\right)\subseteq {G}\right)$