Metamath Proof Explorer

Theorem ttukeylem4

Description: Lemma for ttukey . (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 ttukeylem4 ${⊢}{\phi }\to {G}\left(\varnothing \right)={B}$

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 0elon ${⊢}\varnothing \in \mathrm{On}$
6 1 2 3 4 ttukeylem3 ${⊢}\left({\phi }\wedge \varnothing \in \mathrm{On}\right)\to {G}\left(\varnothing \right)=if\left(\varnothing =\bigcup \varnothing ,if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right),{G}\left(\bigcup \varnothing \right)\cup if\left({G}\left(\bigcup \varnothing \right)\cup \left\{{F}\left(\bigcup \varnothing \right)\right\}\in {A},\left\{{F}\left(\bigcup \varnothing \right)\right\},\varnothing \right)\right)$
7 5 6 mpan2 ${⊢}{\phi }\to {G}\left(\varnothing \right)=if\left(\varnothing =\bigcup \varnothing ,if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right),{G}\left(\bigcup \varnothing \right)\cup if\left({G}\left(\bigcup \varnothing \right)\cup \left\{{F}\left(\bigcup \varnothing \right)\right\}\in {A},\left\{{F}\left(\bigcup \varnothing \right)\right\},\varnothing \right)\right)$
8 uni0 ${⊢}\bigcup \varnothing =\varnothing$
9 8 eqcomi ${⊢}\varnothing =\bigcup \varnothing$
10 9 iftruei ${⊢}if\left(\varnothing =\bigcup \varnothing ,if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right),{G}\left(\bigcup \varnothing \right)\cup if\left({G}\left(\bigcup \varnothing \right)\cup \left\{{F}\left(\bigcup \varnothing \right)\right\}\in {A},\left\{{F}\left(\bigcup \varnothing \right)\right\},\varnothing \right)\right)=if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right)$
11 eqid ${⊢}\varnothing =\varnothing$
12 11 iftruei ${⊢}if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right)={B}$
13 10 12 eqtri ${⊢}if\left(\varnothing =\bigcup \varnothing ,if\left(\varnothing =\varnothing ,{B},\bigcup {G}\left[\varnothing \right]\right),{G}\left(\bigcup \varnothing \right)\cup if\left({G}\left(\bigcup \varnothing \right)\cup \left\{{F}\left(\bigcup \varnothing \right)\right\}\in {A},\left\{{F}\left(\bigcup \varnothing \right)\right\},\varnothing \right)\right)={B}$
14 7 13 syl6eq ${⊢}{\phi }\to {G}\left(\varnothing \right)={B}$