fin23lem26

		Ref	Expression
	Assertion	fin23lem26	$⊢ ((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		breq2	$⊢ i = \emptyset \to ((j \cap S) \approx i \leftrightarrow (j \cap S) \approx \emptyset)$
2	1	rexbidv	$⊢ i = \emptyset \to (\exists j \in S (j \cap S) \approx i \leftrightarrow \exists j \in S (j \cap S) \approx \emptyset)$
3		breq2	$⊢ i = a \to ((j \cap S) \approx i \leftrightarrow (j \cap S) \approx a)$
4	3	rexbidv	$⊢ i = a \to (\exists j \in S (j \cap S) \approx i \leftrightarrow \exists j \in S (j \cap S) \approx a)$
5		breq2	$⊢ i = suc a \to ((j \cap S) \approx i \leftrightarrow (j \cap S) \approx suc a)$
6	5	rexbidv	$⊢ i = suc a \to (\exists j \in S (j \cap S) \approx i \leftrightarrow \exists j \in S (j \cap S) \approx suc a)$
7		ordom	$⊢ Ord ω$
8		simpl	$⊢ (S \subseteq ω \land \neg S \in Fin) \to S \subseteq ω$
9		0fi	$⊢ \emptyset \in Fin$
10		eleq1	$⊢ S = \emptyset \to (S \in Fin \leftrightarrow \emptyset \in Fin)$
11	9 10	mpbiri	$⊢ S = \emptyset \to S \in Fin$
12	11	necon3bi	$⊢ \neg S \in Fin \to S \neq \emptyset$
13	12	adantl	$⊢ (S \subseteq ω \land \neg S \in Fin) \to S \neq \emptyset$
14		tz7.5	$⊢ (Ord ω \land S \subseteq ω \land S \neq \emptyset) \to \exists j \in S S \cap j = \emptyset$
15	7 8 13 14	mp3an2i	$⊢ (S \subseteq ω \land \neg S \in Fin) \to \exists j \in S S \cap j = \emptyset$
16		en0	$⊢ (j \cap S) \approx \emptyset \leftrightarrow j \cap S = \emptyset$
17		incom	$⊢ j \cap S = S \cap j$
18	17	eqeq1i	$⊢ j \cap S = \emptyset \leftrightarrow S \cap j = \emptyset$
19	16 18	bitri	$⊢ (j \cap S) \approx \emptyset \leftrightarrow S \cap j = \emptyset$
20	19	rexbii	$⊢ \exists j \in S (j \cap S) \approx \emptyset \leftrightarrow \exists j \in S S \cap j = \emptyset$
21	15 20	sylibr	$⊢ (S \subseteq ω \land \neg S \in Fin) \to \exists j \in S (j \cap S) \approx \emptyset$
22		simplrl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to S \subseteq ω$
23		omsson	$⊢ ω \subseteq On$
24	22 23	sstrdi	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to S \subseteq On$
25	24	ssdifssd	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to S ∖ suc j \subseteq On$
26		simplr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land j \in S) \to \neg S \in Fin$
27		ssel2	$⊢ (S \subseteq ω \land j \in S) \to j \in ω$
28		onfin2	$⊢ ω = On \cap Fin$
29		inss2	$⊢ On \cap Fin \subseteq Fin$
30	28 29	eqsstri	$⊢ ω \subseteq Fin$
31		peano2	$⊢ j \in ω \to suc j \in ω$
32	30 31	sselid	$⊢ j \in ω \to suc j \in Fin$
33	27 32	syl	$⊢ (S \subseteq ω \land j \in S) \to suc j \in Fin$
34	33	adantlr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land j \in S) \to suc j \in Fin$
35		ssfi	$⊢ (suc j \in Fin \land S \subseteq suc j) \to S \in Fin$
36	35	ex	$⊢ suc j \in Fin \to (S \subseteq suc j \to S \in Fin)$
37	34 36	syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land j \in S) \to (S \subseteq suc j \to S \in Fin)$
38	26 37	mtod	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land j \in S) \to \neg S \subseteq suc j$
39		ssdif0	$⊢ S \subseteq suc j \leftrightarrow S ∖ suc j = \emptyset$
40	39	necon3bbii	$⊢ \neg S \subseteq suc j \leftrightarrow S ∖ suc j \neq \emptyset$
41	38 40	sylib	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land j \in S) \to S ∖ suc j \neq \emptyset$
42	41	ad2ant2lr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to S ∖ suc j \neq \emptyset$
43		onint	$⊢ (S ∖ suc j \subseteq On \land S ∖ suc j \neq \emptyset) \to ⋂ (S ∖ suc j) \in (S ∖ suc j)$
44	25 42 43	syl2anc	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ⋂ (S ∖ suc j) \in (S ∖ suc j)$
45	44	eldifad	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ⋂ (S ∖ suc j) \in S$
46		simprr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (j \cap S) \approx a$
47		en2sn	$⊢ (j \in V \land a \in V) \to \{j\} \approx \{a\}$
48	47	el2v	$⊢ \{j\} \approx \{a\}$
49	48	a1i	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to \{j\} \approx \{a\}$
50		simprl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to j \in S$
51	22 50	sseldd	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to j \in ω$
52		nnord	$⊢ j \in ω \to Ord j$
53	51 52	syl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to Ord j$
54		ordirr	$⊢ Ord j \to \neg j \in j$
55		elinel1	$⊢ j \in (j \cap S) \to j \in j$
56	54 55	nsyl	$⊢ Ord j \to \neg j \in (j \cap S)$
57		disjsn	$⊢ (j \cap S) \cap \{j\} = \emptyset \leftrightarrow \neg j \in (j \cap S)$
58	56 57	sylibr	$⊢ Ord j \to (j \cap S) \cap \{j\} = \emptyset$
59	53 58	syl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (j \cap S) \cap \{j\} = \emptyset$
60		nnord	$⊢ a \in ω \to Ord a$
61		ordirr	$⊢ Ord a \to \neg a \in a$
62	60 61	syl	$⊢ a \in ω \to \neg a \in a$
63		disjsn	$⊢ a \cap \{a\} = \emptyset \leftrightarrow \neg a \in a$
64	62 63	sylibr	$⊢ a \in ω \to a \cap \{a\} = \emptyset$
65	64	ad2antrr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to a \cap \{a\} = \emptyset$
66		unen	$⊢ (((j \cap S) \approx a \land \{j\} \approx \{a\}) \land ((j \cap S) \cap \{j\} = \emptyset \land a \cap \{a\} = \emptyset)) \to ((j \cap S) \cup \{j\}) \approx (a \cup \{a\})$
67	46 49 59 65 66	syl22anc	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ((j \cap S) \cup \{j\}) \approx (a \cup \{a\})$
68		simprr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to b \in S$
69		simplrl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to S \subseteq ω$
70	69 23	sstrdi	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to S \subseteq On$
71		ordsuc	$⊢ Ord j \leftrightarrow Ord suc j$
72	53 71	sylib	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to Ord suc j$
73	72	adantrr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to Ord suc j$
74		simp2	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to S \subseteq On$
75	74	ssdifssd	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to S ∖ suc j \subseteq On$
76		simpl1	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land \neg b \in suc j) \to b \in S$
77		simpr	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land \neg b \in suc j) \to \neg b \in suc j$
78	76 77	eldifd	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land \neg b \in suc j) \to b \in (S ∖ suc j)$
79	78	ex	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to (\neg b \in suc j \to b \in (S ∖ suc j))$
80		onnmin	$⊢ (S ∖ suc j \subseteq On \land b \in (S ∖ suc j)) \to \neg b \in ⋂ (S ∖ suc j)$
81	75 79 80	syl6an	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to (\neg b \in suc j \to \neg b \in ⋂ (S ∖ suc j))$
82	81	con4d	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to (b \in ⋂ (S ∖ suc j) \to b \in suc j)$
83	82	imp	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in ⋂ (S ∖ suc j)) \to b \in suc j$
84		simp3	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to Ord suc j$
85		ordsucss	$⊢ Ord suc j \to (b \in suc j \to suc b \subseteq suc j)$
86	84 85	syl	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to (b \in suc j \to suc b \subseteq suc j)$
87	86	imp	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to suc b \subseteq suc j$
88	87	sscond	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to S ∖ suc j \subseteq S ∖ suc b$
89		intss	$⊢ S ∖ suc j \subseteq S ∖ suc b \to ⋂ (S ∖ suc b) \subseteq ⋂ (S ∖ suc j)$
90	88 89	syl	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to ⋂ (S ∖ suc b) \subseteq ⋂ (S ∖ suc j)$
91		simpl2	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to S \subseteq On$
92		ordelon	$⊢ (Ord suc j \land b \in suc j) \to b \in On$
93	84 92	sylan	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to b \in On$
94		onmindif	$⊢ (S \subseteq On \land b \in On) \to b \in ⋂ (S ∖ suc b)$
95	91 93 94	syl2anc	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to b \in ⋂ (S ∖ suc b)$
96	90 95	sseldd	$⊢ ((b \in S \land S \subseteq On \land Ord suc j) \land b \in suc j) \to b \in ⋂ (S ∖ suc j)$
97	83 96	impbida	$⊢ (b \in S \land S \subseteq On \land Ord suc j) \to (b \in ⋂ (S ∖ suc j) \leftrightarrow b \in suc j)$
98	68 70 73 97	syl3anc	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to (b \in ⋂ (S ∖ suc j) \leftrightarrow b \in suc j)$
99		df-suc	$⊢ suc j = j \cup \{j\}$
100	99	eleq2i	$⊢ b \in suc j \leftrightarrow b \in (j \cup \{j\})$
101	98 100	bitrdi	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land ((j \in S \land (j \cap S) \approx a) \land b \in S)) \to (b \in ⋂ (S ∖ suc j) \leftrightarrow b \in (j \cup \{j\}))$
102	101	expr	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (b \in S \to (b \in ⋂ (S ∖ suc j) \leftrightarrow b \in (j \cup \{j\})))$
103	102	pm5.32rd	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ((b \in ⋂ (S ∖ suc j) \land b \in S) \leftrightarrow (b \in (j \cup \{j\}) \land b \in S))$
104		elin	$⊢ b \in (⋂ (S ∖ suc j) \cap S) \leftrightarrow (b \in ⋂ (S ∖ suc j) \land b \in S)$
105		elin	$⊢ b \in ((j \cup \{j\}) \cap S) \leftrightarrow (b \in (j \cup \{j\}) \land b \in S)$
106	103 104 105	3bitr4g	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (b \in (⋂ (S ∖ suc j) \cap S) \leftrightarrow b \in ((j \cup \{j\}) \cap S))$
107	106	eqrdv	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ⋂ (S ∖ suc j) \cap S = (j \cup \{j\}) \cap S$
108		indir	$⊢ (j \cup \{j\}) \cap S = (j \cap S) \cup (\{j\} \cap S)$
109	107 108	eqtrdi	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ⋂ (S ∖ suc j) \cap S = (j \cap S) \cup (\{j\} \cap S)$
110		snssi	$⊢ j \in S \to \{j\} \subseteq S$
111		dfss2	$⊢ \{j\} \subseteq S \leftrightarrow \{j\} \cap S = \{j\}$
112	110 111	sylib	$⊢ j \in S \to \{j\} \cap S = \{j\}$
113	112	uneq2d	$⊢ j \in S \to (j \cap S) \cup (\{j\} \cap S) = (j \cap S) \cup \{j\}$
114	113	ad2antrl	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (j \cap S) \cup (\{j\} \cap S) = (j \cap S) \cup \{j\}$
115	109 114	eqtrd	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to ⋂ (S ∖ suc j) \cap S = (j \cap S) \cup \{j\}$
116		df-suc	$⊢ suc a = a \cup \{a\}$
117	116	a1i	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to suc a = a \cup \{a\}$
118	67 115 117	3brtr4d	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to (⋂ (S ∖ suc j) \cap S) \approx suc a$
119		ineq1	$⊢ b = ⋂ (S ∖ suc j) \to b \cap S = ⋂ (S ∖ suc j) \cap S$
120	119	breq1d	$⊢ b = ⋂ (S ∖ suc j) \to ((b \cap S) \approx suc a \leftrightarrow (⋂ (S ∖ suc j) \cap S) \approx suc a)$
121	120	rspcev	$⊢ (⋂ (S ∖ suc j) \in S \land (⋂ (S ∖ suc j) \cap S) \approx suc a) \to \exists b \in S (b \cap S) \approx suc a$
122	45 118 121	syl2anc	$⊢ ((a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \land (j \in S \land (j \cap S) \approx a)) \to \exists b \in S (b \cap S) \approx suc a$
123	122	rexlimdvaa	$⊢ (a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \to (\exists j \in S (j \cap S) \approx a \to \exists b \in S (b \cap S) \approx suc a)$
124		ineq1	$⊢ b = j \to b \cap S = j \cap S$
125	124	breq1d	$⊢ b = j \to ((b \cap S) \approx suc a \leftrightarrow (j \cap S) \approx suc a)$
126	125	cbvrexvw	$⊢ \exists b \in S (b \cap S) \approx suc a \leftrightarrow \exists j \in S (j \cap S) \approx suc a$
127	123 126	imbitrdi	$⊢ (a \in ω \land (S \subseteq ω \land \neg S \in Fin)) \to (\exists j \in S (j \cap S) \approx a \to \exists j \in S (j \cap S) \approx suc a)$
128	127	ex	$⊢ a \in ω \to ((S \subseteq ω \land \neg S \in Fin) \to (\exists j \in S (j \cap S) \approx a \to \exists j \in S (j \cap S) \approx suc a))$
129	2 4 6 21 128	finds2	$⊢ i \in ω \to ((S \subseteq ω \land \neg S \in Fin) \to \exists j \in S (j \cap S) \approx i)$
130	129	impcom	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \exists j \in S (j \cap S) \approx i$

Metamath Proof Explorer

Theorem fin23lem26

Proof