fin23lem23

		Ref	Expression
	Assertion	fin23lem23	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \exists! j \in S (j \cap S) \approx i$

Proof

Step	Hyp	Ref	Expression
1		fin23lem26	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \exists j \in S (j \cap S) \approx i$
2		ensym	$⊢ (a \cap S) \approx i \to i \approx (a \cap S)$
3		entr	$⊢ ((j \cap S) \approx i \land i \approx (a \cap S)) \to (j \cap S) \approx (a \cap S)$
4	2 3	sylan2	$⊢ ((j \cap S) \approx i \land (a \cap S) \approx i) \to (j \cap S) \approx (a \cap S)$
5		simpl	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to S \subseteq ω$
6		simprl	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to j \in S$
7	5 6	sseldd	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to j \in ω$
8		nnfi	$⊢ j \in ω \to j \in Fin$
9		inss1	$⊢ j \cap S \subseteq j$
10		ssfi	$⊢ (j \in Fin \land j \cap S \subseteq j) \to j \cap S \in Fin$
11	8 9 10	sylancl	$⊢ j \in ω \to j \cap S \in Fin$
12	7 11	syl	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to j \cap S \in Fin$
13		simprr	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to a \in S$
14	5 13	sseldd	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to a \in ω$
15		nnfi	$⊢ a \in ω \to a \in Fin$
16		inss1	$⊢ a \cap S \subseteq a$
17		ssfi	$⊢ (a \in Fin \land a \cap S \subseteq a) \to a \cap S \in Fin$
18	15 16 17	sylancl	$⊢ a \in ω \to a \cap S \in Fin$
19	14 18	syl	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to a \cap S \in Fin$
20		nnord	$⊢ j \in ω \to Ord j$
21		nnord	$⊢ a \in ω \to Ord a$
22		ordtri2or2	$⊢ (Ord j \land Ord a) \to (j \subseteq a \lor a \subseteq j)$
23	20 21 22	syl2an	$⊢ (j \in ω \land a \in ω) \to (j \subseteq a \lor a \subseteq j)$
24	7 14 23	syl2anc	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to (j \subseteq a \lor a \subseteq j)$
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	$⊢ (j \subseteq a \lor a \subseteq j) \to (j \cap S \subseteq a \cap S \lor a \cap S \subseteq j \cap S)$
28	24 27	syl	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to (j \cap S \subseteq a \cap S \lor a \cap S \subseteq j \cap S)$
29		fin23lem25	$⊢ (j \cap S \in Fin \land a \cap S \in Fin \land (j \cap S \subseteq a \cap S \lor a \cap S \subseteq j \cap S)) \to ((j \cap S) \approx (a \cap S) \leftrightarrow j \cap S = a \cap S)$
30	12 19 28 29	syl3anc	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to ((j \cap S) \approx (a \cap S) \leftrightarrow j \cap S = a \cap S)$
31		ordom	$⊢ Ord ω$
32		fin23lem24	$⊢ ((Ord ω \land S \subseteq ω) \land (j \in S \land a \in S)) \to (j \cap S = a \cap S \leftrightarrow j = a)$
33	31 32	mpanl1	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to (j \cap S = a \cap S \leftrightarrow j = a)$
34	30 33	bitrd	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to ((j \cap S) \approx (a \cap S) \leftrightarrow j = a)$
35	4 34	syl5ib	$⊢ (S \subseteq ω \land (j \in S \land a \in S)) \to (((j \cap S) \approx i \land (a \cap S) \approx i) \to j = a)$
36	35	ralrimivva	$⊢ S \subseteq ω \to \forall j \in S \forall a \in S (((j \cap S) \approx i \land (a \cap S) \approx i) \to j = a)$
37	36	ad2antrr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \forall j \in S \forall a \in S (((j \cap S) \approx i \land (a \cap S) \approx i) \to j = a)$
38		ineq1	$⊢ j = a \to j \cap S = a \cap S$
39	38	breq1d	$⊢ j = a \to ((j \cap S) \approx i \leftrightarrow (a \cap S) \approx i)$
40	39	reu4	$⊢ \exists! j \in S (j \cap S) \approx i \leftrightarrow (\exists j \in S (j \cap S) \approx i \land \forall j \in S \forall a \in S (((j \cap S) \approx i \land (a \cap S) \approx i) \to j = a))$
41	1 37 40	sylanbrc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \exists! j \in S (j \cap S) \approx i$

Metamath Proof Explorer

Theorem fin23lem23

Proof