Theorem 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	⊢ 𝐶 = ( 𝑖 ∈ ω ↦ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) )
Assertion	fin23lem22	⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 : ω –1-1-onto→ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fin23lem22.b	⊢ 𝐶 = ( 𝑖 ∈ ω ↦ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) )
2		fin23lem23	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 )
3		riotacl	⊢ ( ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ∈ 𝑆 )
4	2 3	syl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ∈ 𝑆 )
5		simpll	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑎 ∈ 𝑆 ) → 𝑆 ⊆ ω )
6		simpr	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
7	5 6	sseldd	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ω )
8		nnfi	⊢ ( 𝑎 ∈ ω → 𝑎 ∈ Fin )
9		infi	⊢ ( 𝑎 ∈ Fin → ( 𝑎 ∩ 𝑆 ) ∈ Fin )
10		ficardom	⊢ ( ( 𝑎 ∩ 𝑆 ) ∈ Fin → ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ∈ ω )
11	7 8 9 10	4syl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑎 ∈ 𝑆 ) → ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ∈ ω )
12		cardnn	⊢ ( 𝑖 ∈ ω → ( card ‘ 𝑖 ) = 𝑖 )
13	12	eqcomd	⊢ ( 𝑖 ∈ ω → 𝑖 = ( card ‘ 𝑖 ) )
14	13	eqeq1d	⊢ ( 𝑖 ∈ ω → ( 𝑖 = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ ( card ‘ 𝑖 ) = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ) )
15		eqcom	⊢ ( ( card ‘ 𝑖 ) = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ ( card ‘ ( 𝑎 ∩ 𝑆 ) ) = ( card ‘ 𝑖 ) )
16	14 15	syl6bb	⊢ ( 𝑖 ∈ ω → ( 𝑖 = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ ( card ‘ ( 𝑎 ∩ 𝑆 ) ) = ( card ‘ 𝑖 ) ) )
17	16	ad2antrl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑖 = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ ( card ‘ ( 𝑎 ∩ 𝑆 ) ) = ( card ‘ 𝑖 ) ) )
18		simpll	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑆 ⊆ ω )
19		simprr	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑎 ∈ 𝑆 )
20	18 19	sseldd	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑎 ∈ ω )
21		nnon	⊢ ( 𝑎 ∈ ω → 𝑎 ∈ On )
22		onenon	⊢ ( 𝑎 ∈ On → 𝑎 ∈ dom card )
23	20 21 22	3syl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑎 ∈ dom card )
24		inss1	⊢ ( 𝑎 ∩ 𝑆 ) ⊆ 𝑎
25		ssnum	⊢ ( ( 𝑎 ∈ dom card ∧ ( 𝑎 ∩ 𝑆 ) ⊆ 𝑎 ) → ( 𝑎 ∩ 𝑆 ) ∈ dom card )
26	23 24 25	sylancl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑎 ∩ 𝑆 ) ∈ dom card )
27		nnon	⊢ ( 𝑖 ∈ ω → 𝑖 ∈ On )
28	27	ad2antrl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑖 ∈ On )
29		onenon	⊢ ( 𝑖 ∈ On → 𝑖 ∈ dom card )
30	28 29	syl	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → 𝑖 ∈ dom card )
31		carden2	⊢ ( ( ( 𝑎 ∩ 𝑆 ) ∈ dom card ∧ 𝑖 ∈ dom card ) → ( ( card ‘ ( 𝑎 ∩ 𝑆 ) ) = ( card ‘ 𝑖 ) ↔ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) )
32	26 30 31	syl2anc	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( ( card ‘ ( 𝑎 ∩ 𝑆 ) ) = ( card ‘ 𝑖 ) ↔ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) )
33	2	adantrr	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 )
34		ineq1	⊢ ( 𝑗 = 𝑎 → ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) )
35	34	breq1d	⊢ ( 𝑗 = 𝑎 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) )
36	35	riota2	⊢ ( ( 𝑎 ∈ 𝑆 ∧ ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) → ( ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ↔ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) = 𝑎 ) )
37	19 33 36	syl2anc	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ↔ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) = 𝑎 ) )
38		eqcom	⊢ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) = 𝑎 ↔ 𝑎 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) )
39	37 38	syl6bb	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ↔ 𝑎 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ) )
40	17 32 39	3bitrd	⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑖 = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ 𝑎 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ) )
41	1 4 11 40	f1o2d	⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 : ω –1-1-onto→ 𝑆 )