fin23lem22

Description: Lemma for fin23 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 ) between an infinite subset of _om and _om itself. (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Hypothesis	fin23lem22.b	$⊢ C = (i \in ω ⟼ (ι j \in S \| (j \cap S) \approx i))$
	Assertion	fin23lem22	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C : ω \underset{1-1 onto}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		fin23lem22.b	$⊢ C = (i \in ω ⟼ (ι j \in S \| (j \cap S) \approx i))$
2		fin23lem23	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to \exists! j \in S (j \cap S) \approx i$
3		riotacl	$⊢ \exists! j \in S (j \cap S) \approx i \to (ι j \in S \| (j \cap S) \approx i) \in S$
4	2 3	syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land i \in ω) \to (ι j \in S \| (j \cap S) \approx i) \in S$
5		simpll	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land a \in S) \to S \subseteq ω$
6		simpr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land a \in S) \to a \in S$
7	5 6	sseldd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land a \in S) \to a \in ω$
8		nnfi	$⊢ a \in ω \to a \in Fin$
9		infi	$⊢ a \in Fin \to a \cap S \in Fin$
10		ficardom	$⊢ a \cap S \in Fin \to card (a \cap S) \in ω$
11	7 8 9 10	4syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land a \in S) \to card (a \cap S) \in ω$
12		cardnn	$⊢ i \in ω \to card (i) = i$
13	12	eqcomd	$⊢ i \in ω \to i = card (i)$
14	13	eqeq1d	$⊢ i \in ω \to (i = card (a \cap S) \leftrightarrow card (i) = card (a \cap S))$
15		eqcom	$⊢ card (i) = card (a \cap S) \leftrightarrow card (a \cap S) = card (i)$
16	14 15	bitrdi	$⊢ i \in ω \to (i = card (a \cap S) \leftrightarrow card (a \cap S) = card (i))$
17	16	ad2antrl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to (i = card (a \cap S) \leftrightarrow card (a \cap S) = card (i))$
18		simpll	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to S \subseteq ω$
19		simprr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to a \in S$
20	18 19	sseldd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to a \in ω$
21		nnon	$⊢ a \in ω \to a \in On$
22		onenon	$⊢ a \in On \to a \in dom card$
23	20 21 22	3syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to a \in dom card$
24		inss1	$⊢ a \cap S \subseteq a$
25		ssnum	$⊢ (a \in dom card \land a \cap S \subseteq a) \to a \cap S \in dom card$
26	23 24 25	sylancl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to a \cap S \in dom card$
27		nnon	$⊢ i \in ω \to i \in On$
28	27	ad2antrl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to i \in On$
29		onenon	$⊢ i \in On \to i \in dom card$
30	28 29	syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to i \in dom card$
31		carden2	$⊢ (a \cap S \in dom card \land i \in dom card) \to (card (a \cap S) = card (i) \leftrightarrow (a \cap S) \approx i)$
32	26 30 31	syl2anc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to (card (a \cap S) = card (i) \leftrightarrow (a \cap S) \approx i)$
33	2	adantrr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to \exists! j \in S (j \cap S) \approx i$
34		ineq1	$⊢ j = a \to j \cap S = a \cap S$
35	34	breq1d	$⊢ j = a \to ((j \cap S) \approx i \leftrightarrow (a \cap S) \approx i)$
36	35	riota2	$⊢ (a \in S \land \exists! j \in S (j \cap S) \approx i) \to ((a \cap S) \approx i \leftrightarrow (ι j \in S \| (j \cap S) \approx i) = a)$
37	19 33 36	syl2anc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to ((a \cap S) \approx i \leftrightarrow (ι j \in S \| (j \cap S) \approx i) = a)$
38		eqcom	$⊢ (ι j \in S \| (j \cap S) \approx i) = a \leftrightarrow a = (ι j \in S \| (j \cap S) \approx i)$
39	37 38	bitrdi	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to ((a \cap S) \approx i \leftrightarrow a = (ι j \in S \| (j \cap S) \approx i))$
40	17 32 39	3bitrd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (i \in ω \land a \in S)) \to (i = card (a \cap S) \leftrightarrow a = (ι j \in S \| (j \cap S) \approx i))$
41	1 4 11 40	f1o2d	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C : ω \underset{1-1 onto}{⟶} S$

Metamath Proof Explorer

Theorem fin23lem22

Proof