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𝑆 )