Theorem ttukey2g

Description: The Teichmüller-Tukey Lemma ttukey with a slightly stronger conclusion: we can set up the maximal element of A so that it also contains some given B e. A as a subset. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	ttukey2g	$$⊢\left(\bigcup A\in \mathrm{dom}\mathrm{card}\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\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		difss	$$⊢\bigcup A\setminus B\subseteq \bigcup A$$
2		ssnum	$$⊢\left(\bigcup A\in \mathrm{dom}\mathrm{card}\wedge \bigcup A\setminus B\subseteq \bigcup A\right)\to \bigcup A\setminus B\in \mathrm{dom}\mathrm{card}$$
3	1 2	mpan2	$$⊢\bigcup A\in \mathrm{dom}\mathrm{card}\to \bigcup A\setminus B\in \mathrm{dom}\mathrm{card}$$
4		isnum3	$$⊢\bigcup A\setminus B\in \mathrm{dom}\mathrm{card}\leftrightarrow \mathrm{card}\left(\bigcup A\setminus B\right)\approx \left(\bigcup A\setminus B\right)$$
5		bren	$$⊢\mathrm{card}\left(\bigcup A\setminus B\right)\approx \left(\bigcup A\setminus B\right)\leftrightarrow \exists ff:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B$$
6	4 5	bitri	$$⊢\bigcup A\setminus B\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists ff:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B$$
7		simp1	$$⊢\left(f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B$$
8		simp2	$$⊢\left(f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to B\in A$$
9		simp3	$$⊢\left(f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)$$
10		dmeq	$$⊢w=z\to \mathrm{dom}w=\mathrm{dom}z$$
11	10	unieqd	$$⊢w=z\to \bigcup \mathrm{dom}w=\bigcup \mathrm{dom}z$$
12	10 11	eqeq12d	$$⊢w=z\to \left(\mathrm{dom}w=\bigcup \mathrm{dom}w\leftrightarrow \mathrm{dom}z=\bigcup \mathrm{dom}z\right)$$
13	10	eqeq1d	$$⊢w=z\to \left(\mathrm{dom}w=\varnothing \leftrightarrow \mathrm{dom}z=\varnothing \right)$$
14		rneq	$$⊢w=z\to \mathrm{ran}w=\mathrm{ran}z$$
15	14	unieqd	$$⊢w=z\to \bigcup \mathrm{ran}w=\bigcup \mathrm{ran}z$$
16	13 15	ifbieq2d	$$⊢w=z\to if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right)=if\left(\mathrm{dom}z=\varnothing ,B,\bigcup \mathrm{ran}z\right)$$
17		id	$$⊢w=z\to w=z$$
18	17 11	fveq12d	$$⊢w=z\to w\left(\bigcup \mathrm{dom}w\right)=z\left(\bigcup \mathrm{dom}z\right)$$
19	11	fveq2d	$$⊢w=z\to f\left(\bigcup \mathrm{dom}w\right)=f\left(\bigcup \mathrm{dom}z\right)$$
20	19	sneqd	$$⊢w=z\to \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}=\left\{f\left(\bigcup \mathrm{dom}z\right)\right\}$$
21	18 20	uneq12d	$$⊢w=z\to w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}=z\left(\bigcup \mathrm{dom}z\right)\cup \left\{f\left(\bigcup \mathrm{dom}z\right)\right\}$$
22	21	eleq1d	$$⊢w=z\to \left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A\leftrightarrow z\left(\bigcup \mathrm{dom}z\right)\cup \left\{f\left(\bigcup \mathrm{dom}z\right)\right\}\in A\right)$$
23	22 20	ifbieq1d	$$⊢w=z\to if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\right)\right\},\varnothing \right)=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)$$
24	18 23	uneq12d	$$⊢w=z\to w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\right)\right\},\varnothing \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)$$
25	12 16 24	ifbieq12d	$$⊢w=z\to if\left(\mathrm{dom}w=\bigcup \mathrm{dom}w,if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right),w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\right)\right\},\varnothing \right)\right)=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)$$
26	25	cbvmptv	$$⊢\left(w\in \mathrm{V}⟼if\left(\mathrm{dom}w=\bigcup \mathrm{dom}w,if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right),w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\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)$$
27		recseq	$$⊢\left(w\in \mathrm{V}⟼if\left(\mathrm{dom}w=\bigcup \mathrm{dom}w,if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right),w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\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)\to \mathrm{recs}\left(\left(w\in \mathrm{V}⟼if\left(\mathrm{dom}w=\bigcup \mathrm{dom}w,if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right),w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\right)\right\},\varnothing \right)\right)\right)\right)=\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)$$
28	26 27	ax-mp	$$⊢\mathrm{recs}\left(\left(w\in \mathrm{V}⟼if\left(\mathrm{dom}w=\bigcup \mathrm{dom}w,if\left(\mathrm{dom}w=\varnothing ,B,\bigcup \mathrm{ran}w\right),w\left(\bigcup \mathrm{dom}w\right)\cup if\left(w\left(\bigcup \mathrm{dom}w\right)\cup \left\{f\left(\bigcup \mathrm{dom}w\right)\right\}\in A,\left\{f\left(\bigcup \mathrm{dom}w\right)\right\},\varnothing \right)\right)\right)\right)=\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)$$
29	7 8 9 28	ttukeylem7	$$⊢\left(f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)$$
30	29	3expib	$$⊢f:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\to \left(\left(B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)\right)$$
31	30	exlimiv	$$⊢\exists ff:\mathrm{card}\left(\bigcup A\setminus B\right)\underset{1-1\; onto}{⟶}\bigcup A\setminus B\to \left(\left(B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)\right)$$
32	6 31	sylbi	$$⊢\bigcup A\setminus B\in \mathrm{dom}\mathrm{card}\to \left(\left(B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)\right)$$
33	3 32	syl	$$⊢\bigcup A\in \mathrm{dom}\mathrm{card}\to \left(\left(B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)\right)$$
34	33	3impib	$$⊢\left(\bigcup A\in \mathrm{dom}\mathrm{card}\wedge B\in A\wedge \forall x\left(x\in A\leftrightarrow 𝒫x\cap \mathrm{Fin}\subseteq A\right)\right)\to \exists x\in A\left(B\subseteq x\wedge \forall y\in A\neg x\subset y\right)$$