Theorem fin23lem23

Description: Lemma for fin23lem22 . (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Assertion	fin23lem23	$$⊢\left(\left(S\subseteq \mathrm{\omega }\wedge \neg S\in \mathrm{Fin}\right)\wedge i\in \mathrm{\omega }\right)\to \exists !j\in S\left(j\cap S\right)\approx i$$

Proof

Step	Hyp	Ref	Expression
1		fin23lem26	$$⊢\left(\left(S\subseteq \mathrm{\omega }\wedge \neg S\in \mathrm{Fin}\right)\wedge i\in \mathrm{\omega }\right)\to \exists j\in S\left(j\cap S\right)\approx i$$
2		ensym	$$⊢\left(a\cap S\right)\approx i\to i\approx \left(a\cap S\right)$$
3		entr	$$⊢\left(\left(j\cap S\right)\approx i\wedge i\approx \left(a\cap S\right)\right)\to \left(j\cap S\right)\approx \left(a\cap S\right)$$
4	2 3	sylan2	$$⊢\left(\left(j\cap S\right)\approx i\wedge \left(a\cap S\right)\approx i\right)\to \left(j\cap S\right)\approx \left(a\cap S\right)$$
5		simpl	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to S\subseteq \mathrm{\omega }$$
6		simprl	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to j\in S$$
7	5 6	sseldd	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to j\in \mathrm{\omega }$$
8		nnfi	$$⊢j\in \mathrm{\omega }\to j\in \mathrm{Fin}$$
9		inss1	$$⊢j\cap S\subseteq j$$
10		ssfi	$$⊢\left(j\in \mathrm{Fin}\wedge j\cap S\subseteq j\right)\to j\cap S\in \mathrm{Fin}$$
11	8 9 10	sylancl	$$⊢j\in \mathrm{\omega }\to j\cap S\in \mathrm{Fin}$$
12	7 11	syl	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to j\cap S\in \mathrm{Fin}$$
13		simprr	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to a\in S$$
14	5 13	sseldd	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to a\in \mathrm{\omega }$$
15		nnfi	$$⊢a\in \mathrm{\omega }\to a\in \mathrm{Fin}$$
16		inss1	$$⊢a\cap S\subseteq a$$
17		ssfi	$$⊢\left(a\in \mathrm{Fin}\wedge a\cap S\subseteq a\right)\to a\cap S\in \mathrm{Fin}$$
18	15 16 17	sylancl	$$⊢a\in \mathrm{\omega }\to a\cap S\in \mathrm{Fin}$$
19	14 18	syl	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to a\cap S\in \mathrm{Fin}$$
20		nnord	$$⊢j\in \mathrm{\omega }\to \mathrm{Ord}j$$
21		nnord	$$⊢a\in \mathrm{\omega }\to \mathrm{Ord}a$$
22		ordtri2or2	$$⊢\left(\mathrm{Ord}j\wedge \mathrm{Ord}a\right)\to \left(j\subseteq a\vee a\subseteq j\right)$$
23	20 21 22	syl2an	$$⊢\left(j\in \mathrm{\omega }\wedge a\in \mathrm{\omega }\right)\to \left(j\subseteq a\vee a\subseteq j\right)$$
24	7 14 23	syl2anc	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(j\subseteq a\vee a\subseteq j\right)$$
25		ssrin	$$⊢j\subseteq a\to j\cap S\subseteq a\cap S$$
26		ssrin	$$⊢a\subseteq j\to a\cap S\subseteq j\cap S$$
27	25 26	orim12i	$$⊢\left(j\subseteq a\vee a\subseteq j\right)\to \left(j\cap S\subseteq a\cap S\vee a\cap S\subseteq j\cap S\right)$$
28	24 27	syl	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(j\cap S\subseteq a\cap S\vee a\cap S\subseteq j\cap S\right)$$
29		fin23lem25	$$⊢\left(j\cap S\in \mathrm{Fin}\wedge a\cap S\in \mathrm{Fin}\wedge \left(j\cap S\subseteq a\cap S\vee a\cap S\subseteq j\cap S\right)\right)\to \left(\left(j\cap S\right)\approx \left(a\cap S\right)\leftrightarrow j\cap S=a\cap S\right)$$
30	12 19 28 29	syl3anc	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(\left(j\cap S\right)\approx \left(a\cap S\right)\leftrightarrow j\cap S=a\cap S\right)$$
31		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
32		fin23lem24	$$⊢\left(\left(\mathrm{Ord}\mathrm{\omega }\wedge S\subseteq \mathrm{\omega }\right)\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(j\cap S=a\cap S\leftrightarrow j=a\right)$$
33	31 32	mpanl1	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(j\cap S=a\cap S\leftrightarrow j=a\right)$$
34	30 33	bitrd	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(\left(j\cap S\right)\approx \left(a\cap S\right)\leftrightarrow j=a\right)$$
35	4 34	imbitrid	$$⊢\left(S\subseteq \mathrm{\omega }\wedge \left(j\in S\wedge a\in S\right)\right)\to \left(\left(\left(j\cap S\right)\approx i\wedge \left(a\cap S\right)\approx i\right)\to j=a\right)$$
36	35	ralrimivva	$$⊢S\subseteq \mathrm{\omega }\to \forall j\in S\forall a\in S\left(\left(\left(j\cap S\right)\approx i\wedge \left(a\cap S\right)\approx i\right)\to j=a\right)$$
37	36	ad2antrr	$$⊢\left(\left(S\subseteq \mathrm{\omega }\wedge \neg S\in \mathrm{Fin}\right)\wedge i\in \mathrm{\omega }\right)\to \forall j\in S\forall a\in S\left(\left(\left(j\cap S\right)\approx i\wedge \left(a\cap S\right)\approx i\right)\to j=a\right)$$
38		ineq1	$$⊢j=a\to j\cap S=a\cap S$$
39	38	breq1d	$$⊢j=a\to \left(\left(j\cap S\right)\approx i\leftrightarrow \left(a\cap S\right)\approx i\right)$$
40	39	reu4	$$⊢\exists !j\in S\left(j\cap S\right)\approx i\leftrightarrow \left(\exists j\in S\left(j\cap S\right)\approx i\wedge \forall j\in S\forall a\in S\left(\left(\left(j\cap S\right)\approx i\wedge \left(a\cap S\right)\approx i\right)\to j=a\right)\right)$$
41	1 37 40	sylanbrc	$$⊢\left(\left(S\subseteq \mathrm{\omega }\wedge \neg S\in \mathrm{Fin}\right)\wedge i\in \mathrm{\omega }\right)\to \exists !j\in S\left(j\cap S\right)\approx i$$