Theorem erdszelem1

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	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)$$

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		ovex	$$⊢\left(1\dots A\right)\in \mathrm{V}$$
3	2	elpw2	$$⊢X\in 𝒫\left(1\dots A\right)\leftrightarrow X\subseteq \left(1\dots A\right)$$
4	3	anbi1i	$$⊢\left(X\in 𝒫\left(1\dots A\right)\wedge \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\wedge A\in X\right)\right)\leftrightarrow \left(X\subseteq \left(1\dots A\right)\wedge \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\wedge A\in X\right)\right)$$
5		reseq2	$$⊢y=X\to {F\upharpoonright }_y={F\upharpoonright }_X$$
6		isoeq1	$$⊢{F\upharpoonright }_y={F\upharpoonright }_X\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\right)$$
7	5 6	syl	$$⊢y=X\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\right)$$
8		isoeq4	$$⊢y=X\to \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[y\right]\right)\right)$$
9		imaeq2	$$⊢y=X\to F\left[y\right]=F\left[X\right]$$
10		isoeq5	$$⊢F\left[y\right]=F\left[X\right]\to \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\right)$$
11	9 10	syl	$$⊢y=X\to \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\right)$$
12	7 8 11	3bitrd	$$⊢y=X\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\leftrightarrow \left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\right)$$
13		eleq2	$$⊢y=X\to \left(A\in y\leftrightarrow A\in X\right)$$
14	12 13	anbi12d	$$⊢y=X\to \left(\left(\left({F\upharpoonright }_y\right){Isom}_{<,O}\left(y,F\left[y\right]\right)\wedge A\in y\right)\leftrightarrow \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\wedge A\in X\right)\right)$$
15	14 1	elrab2	$$⊢X\in S\leftrightarrow \left(X\in 𝒫\left(1\dots A\right)\wedge \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\wedge A\in X\right)\right)$$
16		3anass	$$⊢\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)\leftrightarrow \left(X\subseteq \left(1\dots A\right)\wedge \left(\left({F\upharpoonright }_X\right){Isom}_{<,O}\left(X,F\left[X\right]\right)\wedge A\in X\right)\right)$$
17	4 15 16	3bitr4i	$$⊢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)$$