Metamath Proof Explorer

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 bitrdi ⊢ ( 𝑖 ∈ ω → ( 𝑖 = ( 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 bitrdi ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ↔ 𝑎 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ) )
40 17 32 39 3bitrd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑖 = ( card ‘ ( 𝑎 ∩ 𝑆 ) ) ↔ 𝑎 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) ) )
41 1 4 11 40 f1o2d ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 : ω –1-1-onto→ 𝑆 )