Theorem ttukeylem1

Description: Lemma for ttukey . Expand out the property of being an element of a property of finite character. (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)$$
Assertion	ttukeylem1	$$⊢\phi \to \left(C\in A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\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		elex	$$⊢C\in A\to C\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \left(C\in A\to C\in \mathrm{V}\right)$$
6		id	$$⊢𝒫C\cap \mathrm{Fin}\subseteq A\to 𝒫C\cap \mathrm{Fin}\subseteq A$$
7		ssun1	$$⊢\bigcup A\subseteq \bigcup A\cup B$$
8		undif1	$$⊢\left(\bigcup A\setminus B\right)\cup B=\bigcup A\cup B$$
9	7 8	sseqtrri	$$⊢\bigcup A\subseteq \left(\bigcup A\setminus B\right)\cup B$$
10		fvex	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{V}$$
11		f1ofo	$$⊢F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\to F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{onto}{⟶}\bigcup A\setminus B$$
12	1 11	syl	$$⊢\phi \to F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{onto}{⟶}\bigcup A\setminus B$$
13		focdmex	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\in \mathrm{V}\to \left(F:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{onto}{⟶}\bigcup A\setminus B\to \bigcup A\setminus B\in \mathrm{V}\right)$$
14	10 12 13	mpsyl	$$⊢\phi \to \bigcup A\setminus B\in \mathrm{V}$$
15		unexg	$$⊢\left(\bigcup A\setminus B\in \mathrm{V}\wedge B\in A\right)\to \left(\bigcup A\setminus B\right)\cup B\in \mathrm{V}$$
16	14 2 15	syl2anc	$$⊢\phi \to \left(\bigcup A\setminus B\right)\cup B\in \mathrm{V}$$
17		ssexg	$$⊢\left(\bigcup A\subseteq \left(\bigcup A\setminus B\right)\cup B\wedge \left(\bigcup A\setminus B\right)\cup B\in \mathrm{V}\right)\to \bigcup A\in \mathrm{V}$$
18	9 16 17	sylancr	$$⊢\phi \to \bigcup A\in \mathrm{V}$$
19		uniexb	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$
20	18 19	sylibr	$$⊢\phi \to A\in \mathrm{V}$$
21		ssexg	$$⊢\left(𝒫C\cap \mathrm{Fin}\subseteq A\wedge A\in \mathrm{V}\right)\to 𝒫C\cap \mathrm{Fin}\in \mathrm{V}$$
22	6 20 21	syl2anr	$$⊢\left(\phi \wedge 𝒫C\cap \mathrm{Fin}\subseteq A\right)\to 𝒫C\cap \mathrm{Fin}\in \mathrm{V}$$
23		infpwfidom	$$⊢𝒫C\cap \mathrm{Fin}\in \mathrm{V}\to C\preccurlyeq \left(𝒫C\cap \mathrm{Fin}\right)$$
24		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
25	24	brrelex1i	$$⊢C\preccurlyeq \left(𝒫C\cap \mathrm{Fin}\right)\to C\in \mathrm{V}$$
26	22 23 25	3syl	$$⊢\left(\phi \wedge 𝒫C\cap \mathrm{Fin}\subseteq A\right)\to C\in \mathrm{V}$$
27	26	ex	$$⊢\phi \to \left(𝒫C\cap \mathrm{Fin}\subseteq A\to C\in \mathrm{V}\right)$$
28		eleq1	$$⊢x=C\to \left(x\in A\leftrightarrow C\in A\right)$$
29		pweq	$$⊢x=C\to 𝒫x=𝒫C$$
30	29	ineq1d	$$⊢x=C\to 𝒫x\cap \mathrm{Fin}=𝒫C\cap \mathrm{Fin}$$
31	30	sseq1d	$$⊢x=C\to \left(𝒫x\cap \mathrm{Fin}\subseteq A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\right)$$
32	28 31	bibi12d	$$⊢x=C\to \left(\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\leftrightarrow \left(C\in A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\right)\right)$$
33	32	spcgv	$$⊢C\in \mathrm{V}\to \left(\forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\to \left(C\in A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\right)\right)$$
34	3 33	syl5com	$$⊢\phi \to \left(C\in \mathrm{V}\to \left(C\in A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\right)\right)$$
35	5 27 34	pm5.21ndd	$$⊢\phi \to \left(C\in A\leftrightarrow 𝒫C\cap \mathrm{Fin}\subseteq A\right)$$