Theorem ttukeylem7

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\left(x\in A\leftrightarrow 𝒫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	ttukeylem7	$$⊢\phi \to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\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\left(x\in A\leftrightarrow 𝒫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		fvex	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{V}$$
6	5	sucid	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{suc}\mathrm{card}\left(\bigcup A\setminus B\right)$$
7	1 2 3 4	ttukeylem6	$$⊢\left(\phi \wedge \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{suc}\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\in A$$
8	6 7	mpan2	$$⊢\phi \to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\in A$$
9	1 2 3 4	ttukeylem4	$$⊢\phi \to G\left(\varnothing \right)=B$$
10		0elon	$$⊢\varnothing \in \mathrm{On}$$
11		cardon	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}$$
12		0ss	$$⊢\varnothing \subseteq \mathrm{card}\left(\bigcup A\setminus B\right)$$
13	10 11 12	3pm3.2i	$$⊢\left(\varnothing \in \mathrm{On}\wedge \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}\wedge \varnothing \subseteq \mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
14	1 2 3 4	ttukeylem5	$$⊢\left(\phi \wedge \left(\varnothing \in \mathrm{On}\wedge \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}\wedge \varnothing \subseteq \mathrm{card}\left(\bigcup A\setminus B\right)\right)\right)\to G\left(\varnothing \right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
15	13 14	mpan2	$$⊢\phi \to G\left(\varnothing \right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
16	9 15	eqsstrrd	$$⊢\phi \to B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
17		simprr	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y$$
18		ssun1	$$⊢y\subseteq y\cup B$$
19		undif1	$$⊢\left(y\setminus B\right)\cup B=y\cup B$$
20	18 19	sseqtrri	$$⊢y\subseteq \left(y\setminus B\right)\cup B$$
21		simpl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \phi$$
22		f1ocnv	$$⊢F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\to F^{-1}:\bigcup A\setminus B\underset{1-1\; onto}{⟶}\mathrm{card}\left(\bigcup A\setminus B\right)$$
23		f1of	$$⊢F^{-1}:\bigcup A\setminus B\underset{1-1\; onto}{⟶}\mathrm{card}\left(\bigcup A\setminus B\right)\to F^{-1}:\bigcup A\setminus B⟶\mathrm{card}\left(\bigcup A\setminus B\right)$$
24	1 22 23	3syl	$$⊢\phi \to F^{-1}:\bigcup A\setminus B⟶\mathrm{card}\left(\bigcup A\setminus B\right)$$
25	24	adantr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F^{-1}:\bigcup A\setminus B⟶\mathrm{card}\left(\bigcup A\setminus B\right)$$
26		eldifi	$$⊢a\in \left(y\setminus B\right)\to a\in y$$
27	26	ad2antll	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in y$$
28		simprll	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to y\in A$$
29		elunii	$$⊢\left(a\in y\wedge y\in A\right)\to a\in \bigcup A$$
30	27 28 29	syl2anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in \bigcup A$$
31		eldifn	$$⊢a\in \left(y\setminus B\right)\to \neg a\in B$$
32	31	ad2antll	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \neg a\in B$$
33	30 32	eldifd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in \left(\bigcup A\setminus B\right)$$
34	25 33	ffvelcdmd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F^{-1}\left(a\right)\in \mathrm{card}\left(\bigcup A\setminus B\right)$$
35		onelon	$$⊢\left(\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}\wedge F^{-1}\left(a\right)\in \mathrm{card}\left(\bigcup A\setminus B\right)\right)\to F^{-1}\left(a\right)\in \mathrm{On}$$
36	11 34 35	sylancr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F^{-1}\left(a\right)\in \mathrm{On}$$
37		onsuc	$$⊢F^{-1}\left(a\right)\in \mathrm{On}\to \mathrm{suc}{F}^{-1}\left(a\right)\in \mathrm{On}$$
38	36 37	syl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\in \mathrm{On}$$
39	11	a1i	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}$$
40	11	onordi	$$⊢\mathrm{Ord}\mathrm{card}\left(\bigcup A\setminus B\right)$$
41		ordsucss	$$⊢\mathrm{Ord}\mathrm{card}\left(\bigcup A\setminus B\right)\to \left(F^{-1}\left(a\right)\in \mathrm{card}\left(\bigcup A\setminus B\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
42	40 34 41	mpsyl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)$$
43	1 2 3 4	ttukeylem5	$$⊢\left(\phi \wedge \left(\mathrm{suc}{F}^{-1}\left(a\right)\in \mathrm{On}\wedge \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}\wedge \mathrm{suc}{F}^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)\right)\right)\to G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
44	21 38 39 42 43	syl13anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
45		ssun2	$$⊢if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)\subseteq G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)$$
46		eloni	$$⊢F^{-1}\left(a\right)\in \mathrm{On}\to \mathrm{Ord}{F}^{-1}\left(a\right)$$
47		ordunisuc	$$⊢\mathrm{Ord}{F}^{-1}\left(a\right)\to \bigcup \mathrm{suc}{F}^{-1}\left(a\right)=F^{-1}\left(a\right)$$
48	36 46 47	3syl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \bigcup \mathrm{suc}{F}^{-1}\left(a\right)=F^{-1}\left(a\right)$$
49	48	fveq2d	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)=F\left(F^{-1}\left(a\right)\right)$$
50	1	adantr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B$$
51		f1ocnvfv2	$$⊢\left(F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\wedge a\in \left(\bigcup A\setminus B\right)\right)\to F\left(F^{-1}\left(a\right)\right)=a$$
52	50 33 51	syl2anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F\left(F^{-1}\left(a\right)\right)=a$$
53	49 52	eqtr2d	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a=F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)$$
54		velsn	$$⊢a\in \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\leftrightarrow a=F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)$$
55	53 54	sylibr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}$$
56	48	fveq2d	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)=G\left(F^{-1}\left(a\right)\right)$$
57		ordelss	$$⊢\left(\mathrm{Ord}\mathrm{card}\left(\bigcup A\setminus B\right)\wedge F^{-1}\left(a\right)\in \mathrm{card}\left(\bigcup A\setminus B\right)\right)\to F^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)$$
58	40 34 57	sylancr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)$$
59	1 2 3 4	ttukeylem5	$$⊢\left(\phi \wedge \left(F^{-1}\left(a\right)\in \mathrm{On}\wedge \mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{On}\wedge F^{-1}\left(a\right)\subseteq \mathrm{card}\left(\bigcup A\setminus B\right)\right)\right)\to G\left(F^{-1}\left(a\right)\right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
60	21 36 39 58 59	syl13anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(F^{-1}\left(a\right)\right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
61	56 60	eqsstrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
62		simprlr	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y$$
63	61 62	sstrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\subseteq y$$
64	53 27	eqeltrrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\in y$$
65	64	snssd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\subseteq y$$
66	63 65	unssd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\subseteq y$$
67	1 2 3	ttukeylem2	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\subseteq y\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A$$
68	21 28 66 67	syl12anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A$$
69	68	iftrued	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)=\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}$$
70	55 69	eleqtrrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)$$
71	45 70	sselid	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in \left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)\right)$$
72	1 2 3 4	ttukeylem3	$$⊢\left(\phi \wedge \mathrm{suc}{F}^{-1}\left(a\right)\in \mathrm{On}\right)\to G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)=if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\bigcup \mathrm{suc}{F}^{-1}\left(a\right),if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\varnothing ,B,\bigcup G\left[\mathrm{suc}{F}^{-1}\left(a\right)\right]\right),G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)\right)$$
73	38 72	syldan	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)=if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\bigcup \mathrm{suc}{F}^{-1}\left(a\right),if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\varnothing ,B,\bigcup G\left[\mathrm{suc}{F}^{-1}\left(a\right)\right]\right),G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)\right)$$
74		sucidg	$$⊢F^{-1}\left(a\right)\in \mathrm{card}\left(\bigcup A\setminus B\right)\to F^{-1}\left(a\right)\in \mathrm{suc}{F}^{-1}\left(a\right)$$
75	34 74	syl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to F^{-1}\left(a\right)\in \mathrm{suc}{F}^{-1}\left(a\right)$$
76		ordirr	$$⊢\mathrm{Ord}{F}^{-1}\left(a\right)\to \neg F^{-1}\left(a\right)\in F^{-1}\left(a\right)$$
77	36 46 76	3syl	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \neg F^{-1}\left(a\right)\in F^{-1}\left(a\right)$$
78		nelne1	$$⊢\left(F^{-1}\left(a\right)\in \mathrm{suc}{F}^{-1}\left(a\right)\wedge \neg F^{-1}\left(a\right)\in F^{-1}\left(a\right)\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\ne F^{-1}\left(a\right)$$
79	75 77 78	syl2anc	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\ne F^{-1}\left(a\right)$$
80	79 48	neeqtrrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \mathrm{suc}{F}^{-1}\left(a\right)\ne \bigcup \mathrm{suc}{F}^{-1}\left(a\right)$$
81	80	neneqd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to \neg \mathrm{suc}{F}^{-1}\left(a\right)=\bigcup \mathrm{suc}{F}^{-1}\left(a\right)$$
82	81	iffalsed	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\bigcup \mathrm{suc}{F}^{-1}\left(a\right),if\left(\mathrm{suc}{F}^{-1}\left(a\right)=\varnothing ,B,\bigcup G\left[\mathrm{suc}{F}^{-1}\left(a\right)\right]\right),G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)\right)=G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)$$
83	73 82	eqtrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)=G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup if\left(G\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\cup \left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\}\in A,\left\{F\left(\bigcup \mathrm{suc}{F}^{-1}\left(a\right)\right)\right\},\varnothing \right)$$
84	71 83	eleqtrrd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in G\left(\mathrm{suc}{F}^{-1}\left(a\right)\right)$$
85	44 84	sseldd	$$⊢\left(\phi \wedge \left(\left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\wedge a\in \left(y\setminus B\right)\right)\right)\to a\in G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
86	85	expr	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to \left(a\in \left(y\setminus B\right)\to a\in G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\right)$$
87	86	ssrdv	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to y\setminus B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
88	16	adantr	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
89	87 88	unssd	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to \left(y\setminus B\right)\cup B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
90	20 89	sstrid	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to y\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)$$
91	17 90	eqssd	$$⊢\left(\phi \wedge \left(y\in A\wedge G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\right)\right)\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)=y$$
92	91	expr	$$⊢\left(\phi \wedge y\in A\right)\to \left(G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)=y\right)$$
93		npss	$$⊢\neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\leftrightarrow \left(G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subseteq y\to G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)=y\right)$$
94	92 93	sylibr	$$⊢\left(\phi \wedge y\in A\right)\to \neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y$$
95	94	ralrimiva	$$⊢\phi \to \forall y\in A\neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y$$
96		sseq2	$$⊢x=G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to \left(B\subseteq x\leftrightarrow B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\right)$$
97		psseq1	$$⊢x=G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to \left(x\subset y\leftrightarrow G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\right)$$
98	97	notbid	$$⊢x=G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to \left(\neg x\subset y\leftrightarrow \neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\right)$$
99	98	ralbidv	$$⊢x=G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to \left(\forall y\in A\neg x\subset y\leftrightarrow \forall y\in A\neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\right)$$
100	96 99	anbi12d	$$⊢x=G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\to \left(\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)\leftrightarrow \left(B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\wedge \forall y\in A\neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\right)\right)$$
101	100	rspcev	$$⊢\left(G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\in A\wedge \left(B\subseteq G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\wedge \forall y\in A\neg G\left(\mathrm{card}\left(\bigcup A\setminus B\right)\right)\subset y\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)$$
102	8 16 95 101	syl12anc	$$⊢\phi \to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)$$