# Metamath Proof Explorer

## Theorem ttukeylem3

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 11-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 ttukeylem3 ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to {G}\left({C}\right)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\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 4 tfr2 ${⊢}{C}\in \mathrm{On}\to {G}\left({C}\right)=\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)\left({{G}↾}_{{C}}\right)$
6 5 adantl ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to {G}\left({C}\right)=\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)\left({{G}↾}_{{C}}\right)$
7 eqidd ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \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)=\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)$
8 simpr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {z}={{G}↾}_{{C}}$
9 8 dmeqd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{dom}{z}=\mathrm{dom}\left({{G}↾}_{{C}}\right)$
10 4 tfr1 ${⊢}{G}Fn\mathrm{On}$
11 onss ${⊢}{C}\in \mathrm{On}\to {C}\subseteq \mathrm{On}$
12 11 ad2antlr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {C}\subseteq \mathrm{On}$
13 fnssres ${⊢}\left({G}Fn\mathrm{On}\wedge {C}\subseteq \mathrm{On}\right)\to \left({{G}↾}_{{C}}\right)Fn{C}$
14 10 12 13 sylancr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left({{G}↾}_{{C}}\right)Fn{C}$
15 fndm ${⊢}\left({{G}↾}_{{C}}\right)Fn{C}\to \mathrm{dom}\left({{G}↾}_{{C}}\right)={C}$
16 14 15 syl ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{dom}\left({{G}↾}_{{C}}\right)={C}$
17 9 16 eqtrd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{dom}{z}={C}$
18 17 unieqd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \bigcup \mathrm{dom}{z}=\bigcup {C}$
19 17 18 eqeq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left(\mathrm{dom}{z}=\bigcup \mathrm{dom}{z}↔{C}=\bigcup {C}\right)$
20 17 eqeq1d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left(\mathrm{dom}{z}=\varnothing ↔{C}=\varnothing \right)$
21 8 rneqd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{ran}{z}=\mathrm{ran}\left({{G}↾}_{{C}}\right)$
22 df-ima ${⊢}{G}\left[{C}\right]=\mathrm{ran}\left({{G}↾}_{{C}}\right)$
23 21 22 syl6eqr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{ran}{z}={G}\left[{C}\right]$
24 23 unieqd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \bigcup \mathrm{ran}{z}=\bigcup {G}\left[{C}\right]$
25 20 24 ifbieq2d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to if\left(\mathrm{dom}{z}=\varnothing ,{B},\bigcup \mathrm{ran}{z}\right)=if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right)$
26 8 18 fveq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {z}\left(\bigcup \mathrm{dom}{z}\right)=\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)$
27 18 fveq2d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {F}\left(\bigcup \mathrm{dom}{z}\right)={F}\left(\bigcup {C}\right)$
28 27 sneqd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\}=\left\{{F}\left(\bigcup {C}\right)\right\}$
29 26 28 uneq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {z}\left(\bigcup \mathrm{dom}{z}\right)\cup \left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\}=\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}$
30 29 eleq1d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left({z}\left(\bigcup \mathrm{dom}{z}\right)\cup \left\{{F}\left(\bigcup \mathrm{dom}{z}\right)\right\}\in {A}↔\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A}\right)$
31 eqidd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \varnothing =\varnothing$
32 30 28 31 ifbieq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to 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)=if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)$
33 26 32 uneq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to {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)=\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)$
34 19 25 33 ifbieq12d ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to 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)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)$
35 onuni ${⊢}{C}\in \mathrm{On}\to \bigcup {C}\in \mathrm{On}$
36 35 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \bigcup {C}\in \mathrm{On}$
37 sucidg ${⊢}\bigcup {C}\in \mathrm{On}\to \bigcup {C}\in \mathrm{suc}\bigcup {C}$
38 36 37 syl ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \bigcup {C}\in \mathrm{suc}\bigcup {C}$
39 eloni ${⊢}{C}\in \mathrm{On}\to \mathrm{Ord}{C}$
40 39 ad2antlr ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \mathrm{Ord}{C}$
41 orduniorsuc ${⊢}\mathrm{Ord}{C}\to \left({C}=\bigcup {C}\vee {C}=\mathrm{suc}\bigcup {C}\right)$
42 40 41 syl ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to \left({C}=\bigcup {C}\vee {C}=\mathrm{suc}\bigcup {C}\right)$
43 42 orcanai ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to {C}=\mathrm{suc}\bigcup {C}$
44 38 43 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \bigcup {C}\in {C}$
45 44 fvresd ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)={G}\left(\bigcup {C}\right)$
46 45 uneq1d ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}={G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}$
47 46 eleq1d ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A}↔{G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A}\right)$
48 47 ifbid ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)=if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)$
49 45 48 uneq12d ${⊢}\left(\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\wedge ¬{C}=\bigcup {C}\right)\to \left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)={G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)$
50 49 ifeq2da ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup if\left(\left({{G}↾}_{{C}}\right)\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)$
51 34 50 eqtrd ${⊢}\left(\left({\phi }\wedge {C}\in \mathrm{On}\right)\wedge {z}={{G}↾}_{{C}}\right)\to 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)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)$
52 fnfun ${⊢}{G}Fn\mathrm{On}\to \mathrm{Fun}{G}$
53 10 52 ax-mp ${⊢}\mathrm{Fun}{G}$
54 simpr ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to {C}\in \mathrm{On}$
55 resfunexg ${⊢}\left(\mathrm{Fun}{G}\wedge {C}\in \mathrm{On}\right)\to {{G}↾}_{{C}}\in \mathrm{V}$
56 53 54 55 sylancr ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to {{G}↾}_{{C}}\in \mathrm{V}$
57 2 elexd ${⊢}{\phi }\to {B}\in \mathrm{V}$
58 funimaexg ${⊢}\left(\mathrm{Fun}{G}\wedge {C}\in \mathrm{On}\right)\to {G}\left[{C}\right]\in \mathrm{V}$
59 53 58 mpan ${⊢}{C}\in \mathrm{On}\to {G}\left[{C}\right]\in \mathrm{V}$
60 59 uniexd ${⊢}{C}\in \mathrm{On}\to \bigcup {G}\left[{C}\right]\in \mathrm{V}$
61 ifcl ${⊢}\left({B}\in \mathrm{V}\wedge \bigcup {G}\left[{C}\right]\in \mathrm{V}\right)\to if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right)\in \mathrm{V}$
62 57 60 61 syl2an ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right)\in \mathrm{V}$
63 fvex ${⊢}{G}\left(\bigcup {C}\right)\in \mathrm{V}$
64 snex ${⊢}\left\{{F}\left(\bigcup {C}\right)\right\}\in \mathrm{V}$
65 0ex ${⊢}\varnothing \in \mathrm{V}$
66 64 65 ifex ${⊢}if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\in \mathrm{V}$
67 63 66 unex ${⊢}{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\in \mathrm{V}$
68 ifcl ${⊢}\left(if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right)\in \mathrm{V}\wedge {G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\in \mathrm{V}\right)\to if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)\in \mathrm{V}$
69 62 67 68 sylancl ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)\in \mathrm{V}$
70 7 51 56 69 fvmptd ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to \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)\left({{G}↾}_{{C}}\right)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)$
71 6 70 eqtrd ${⊢}\left({\phi }\wedge {C}\in \mathrm{On}\right)\to {G}\left({C}\right)=if\left({C}=\bigcup {C},if\left({C}=\varnothing ,{B},\bigcup {G}\left[{C}\right]\right),{G}\left(\bigcup {C}\right)\cup if\left({G}\left(\bigcup {C}\right)\cup \left\{{F}\left(\bigcup {C}\right)\right\}\in {A},\left\{{F}\left(\bigcup {C}\right)\right\},\varnothing \right)\right)$