Theorem erdszelem2

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypothesis	erdszelem1.1	$$⊢S=\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}$$
Assertion	erdszelem2	$$⊢\left(\left|.\right|\left[S\right]\in \mathrm{Fin}\wedge \left|.\right|\left[S\right]\subseteq \mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		erdszelem1.1	$$⊢S=\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}$$
2		fzfi	$$⊢\left(1\dots A\right)\in \mathrm{Fin}$$
3		pwfi	$$⊢\left(1\dots A\right)\in \mathrm{Fin}\leftrightarrow 𝒫\left(1\dots A\right)\in \mathrm{Fin}$$
4	2 3	mpbi	$$⊢𝒫\left(1\dots A\right)\in \mathrm{Fin}$$
5		ssrab2	$$⊢\left\{y\in 𝒫\left(1\dots A\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\right\}\subseteq 𝒫\left(1\dots A\right)$$
6	1 5	eqsstri	$$⊢S\subseteq 𝒫\left(1\dots A\right)$$
7		ssfi	$$⊢\left(𝒫\left(1\dots A\right)\in \mathrm{Fin}\wedge S\subseteq 𝒫\left(1\dots A\right)\right)\to S\in \mathrm{Fin}$$
8	4 6 7	mp2an	$$⊢S\in \mathrm{Fin}$$
9		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
10		ffun	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \mathrm{Fun}\left|.\right|$$
11	9 10	ax-mp	$$⊢\mathrm{Fun}\left|.\right|$$
12		ssv	$$⊢S\subseteq \mathrm{V}$$
13	9	fdmi	$$⊢\mathrm{dom}\left|.\right|=\mathrm{V}$$
14	12 13	sseqtrri	$$⊢S\subseteq \mathrm{dom}\left|.\right|$$
15		fores	$$⊢\left(\mathrm{Fun}\left|.\right|\wedge S\subseteq \mathrm{dom}\left|.\right|\right)\to \left({\left|.\right|\upharpoonright }_S\right):S\underset{onto}{⟶}\left|.\right|\left[S\right]$$
16	11 14 15	mp2an	$$⊢\left({\left|.\right|\upharpoonright }_S\right):S\underset{onto}{⟶}\left|.\right|\left[S\right]$$
17		fofi	$$⊢\left(S\in \mathrm{Fin}\wedge \left({\left|.\right|\upharpoonright }_S\right):S\underset{onto}{⟶}\left|.\right|\left[S\right]\right)\to \left|.\right|\left[S\right]\in \mathrm{Fin}$$
18	8 16 17	mp2an	$$⊢\left|.\right|\left[S\right]\in \mathrm{Fin}$$
19		funimass4	$$⊢\left(\mathrm{Fun}\left|.\right|\wedge S\subseteq \mathrm{dom}\left|.\right|\right)\to \left(\left|.\right|\left[S\right]\subseteq \mathbb{N}\leftrightarrow \forall x\in S\left|x\right|\in \mathbb{N}\right)$$
20	11 14 19	mp2an	$$⊢\left|.\right|\left[S\right]\subseteq \mathbb{N}\leftrightarrow \forall x\in S\left|x\right|\in \mathbb{N}$$
21	1	erdszelem1	$$⊢x\in S\leftrightarrow \left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)$$
22		ne0i	$$⊢A\in x\to x\ne \varnothing$$
23	22	3ad2ant3	$$⊢\left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)\to x\ne \varnothing$$
24		simp1	$$⊢\left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)\to x\subseteq \left(1\dots A\right)$$
25		ssfi	$$⊢\left(\left(1\dots A\right)\in \mathrm{Fin}\wedge x\subseteq \left(1\dots A\right)\right)\to x\in \mathrm{Fin}$$
26	2 24 25	sylancr	$$⊢\left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)\to x\in \mathrm{Fin}$$
27		hashnncl	$$⊢x\in \mathrm{Fin}\to \left(\left|x\right|\in \mathbb{N}\leftrightarrow x\ne \varnothing \right)$$
28	26 27	syl	$$⊢\left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)\to \left(\left|x\right|\in \mathbb{N}\leftrightarrow x\ne \varnothing \right)$$
29	23 28	mpbird	$$⊢\left(x\subseteq \left(1\dots A\right)\wedge \left({F\upharpoonright }_x\right){Isom}_{<,O}\left(x,F\left[x\right]\right)\wedge A\in x\right)\to \left|x\right|\in \mathbb{N}$$
30	21 29	sylbi	$$⊢x\in S\to \left|x\right|\in \mathbb{N}$$
31	20 30	mprgbir	$$⊢\left|.\right|\left[S\right]\subseteq \mathbb{N}$$
32	18 31	pm3.2i	$$⊢\left(\left|.\right|\left[S\right]\in \mathrm{Fin}\wedge \left|.\right|\left[S\right]\subseteq \mathbb{N}\right)$$