This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin23lem27

Description: The mapping constructed in fin23lem22 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem22.b ⊢ 𝐶 = ( 𝑖 ∈ ω ↦ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) )
Assertion fin23lem27 ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 Isom E , E ( ω , 𝑆 ) )

Proof

Step Hyp Ref Expression
1 fin23lem22.b ⊢ 𝐶 = ( 𝑖 ∈ ω ↦ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) )
2 ordom ⊢ Ord ω
3 ordwe ⊢ ( Ord ω → E We ω )
4 weso ⊢ ( E We ω → E Or ω )
5 2 3 4 mp2b ⊢ E Or ω
6 5 a1i ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → E Or ω )
7 sopo ⊢ ( E Or ω → E Po ω )
8 5 7 ax-mp ⊢ E Po ω
9 poss ⊢ ( 𝑆 ⊆ ω → ( E Po ω → E Po 𝑆 ) )
10 8 9 mpi ⊢ ( 𝑆 ⊆ ω → E Po 𝑆 )
11 10 adantr ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → E Po 𝑆 )
12 1 fin23lem22 ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 : ω –1-1-onto→ 𝑆 )
13 f1ofo ⊢ ( 𝐶 : ω –1-1-onto→ 𝑆 → 𝐶 : ω –onto→ 𝑆 )
14 12 13 syl ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 : ω –onto→ 𝑆 )
15 nnsdomel ⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( 𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏 ) )
16 15 adantl ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏 ) )
17 16 biimpd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏 ) )
18 fin23lem23 ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑎 ∈ ω ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 )
19 18 adantrr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 )
20 ineq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∩ 𝑆 ) = ( 𝑖 ∩ 𝑆 ) )
21 20 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ↔ ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 ) )
22 21 cbvreuvw ⊢ ( ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ↔ ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 )
23 19 22 sylib ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 )
24 nfv ⊢ Ⅎ 𝑖 ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎
25 21 cbvriotavw ⊢ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) = ( ℩ 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 )
26 ineq1 ⊢ ( 𝑖 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) → ( 𝑖 ∩ 𝑆 ) = ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) )
27 26 breq1d ⊢ ( 𝑖 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) → ( ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 ↔ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 ) )
28 24 25 27 riotaprop ⊢ ( ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑎 → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ 𝑆 ∧ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 ) )
29 23 28 syl ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ 𝑆 ∧ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 ) )
30 29 simprd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 )
31 30 adantrr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑎 ≺ 𝑏 ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 )
32 simprr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑎 ≺ 𝑏 ) ) → 𝑎 ≺ 𝑏 )
33 fin23lem23 ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑏 ∈ ω ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 )
34 33 adantrl ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 )
35 20 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ↔ ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 ) )
36 35 cbvreuvw ⊢ ( ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ↔ ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 )
37 34 36 sylib ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 )
38 nfv ⊢ Ⅎ 𝑖 ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ≈ 𝑏
39 35 cbvriotavw ⊢ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) = ( ℩ 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 )
40 ineq1 ⊢ ( 𝑖 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) → ( 𝑖 ∩ 𝑆 ) = ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
41 40 breq1d ⊢ ( 𝑖 = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) → ( ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 ↔ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ≈ 𝑏 ) )
42 38 39 41 riotaprop ⊢ ( ∃! 𝑖 ∈ 𝑆 ( 𝑖 ∩ 𝑆 ) ≈ 𝑏 → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ 𝑆 ∧ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ≈ 𝑏 ) )
43 37 42 syl ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ 𝑆 ∧ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ≈ 𝑏 ) )
44 43 simprd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ≈ 𝑏 )
45 44 ensymd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → 𝑏 ≈ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
46 45 adantrr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑎 ≺ 𝑏 ) ) → 𝑏 ≈ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
47 sdomentr ⊢ ( ( 𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ) → 𝑎 ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
48 32 46 47 syl2anc ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑎 ≺ 𝑏 ) ) → 𝑎 ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
49 ensdomtr ⊢ ( ( ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≈ 𝑎 ∧ 𝑎 ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
50 31 48 49 syl2anc ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ 𝑎 ≺ 𝑏 ) ) → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) )
51 50 expr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 ≺ 𝑏 → ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ) )
52 simpll ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → 𝑆 ⊆ ω )
53 omsson ⊢ ω ⊆ On
54 52 53 sstrdi ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → 𝑆 ⊆ On )
55 29 simpld ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ 𝑆 )
56 54 55 sseldd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ On )
57 43 simpld ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ 𝑆 )
58 54 57 sseldd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ On )
59 onsdominel ⊢ ( ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ On ∧ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ On ∧ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) )
60 59 3expia ⊢ ( ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ On ∧ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∈ On ) → ( ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ) )
61 56 58 60 syl2anc ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∩ 𝑆 ) ≺ ( ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ∩ 𝑆 ) → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ) )
62 17 51 61 3syld ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 ∈ 𝑏 → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ) )
63 breq2 ⊢ ( 𝑖 = 𝑎 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) )
64 63 riotabidv ⊢ ( 𝑖 = 𝑎 → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) )
65 simprl ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → 𝑎 ∈ ω )
66 1 64 65 55 fvmptd3 ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝐶 ‘ 𝑎 ) = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) )
67 breq2 ⊢ ( 𝑖 = 𝑏 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) )
68 67 riotabidv ⊢ ( 𝑖 = 𝑏 → ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) )
69 simprr ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → 𝑏 ∈ ω )
70 1 68 69 57 fvmptd3 ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝐶 ‘ 𝑏 ) = ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) )
71 66 70 eleq12d ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( ( 𝐶 ‘ 𝑎 ) ∈ ( 𝐶 ‘ 𝑏 ) ↔ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑎 ) ∈ ( ℩ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑏 ) ) )
72 62 71 sylibrd ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 ∈ 𝑏 → ( 𝐶 ‘ 𝑎 ) ∈ ( 𝐶 ‘ 𝑏 ) ) )
73 epel ⊢ ( 𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏 )
74 fvex ⊢ ( 𝐶 ‘ 𝑏 ) ∈ V
75 74 epeli ⊢ ( ( 𝐶 ‘ 𝑎 ) E ( 𝐶 ‘ 𝑏 ) ↔ ( 𝐶 ‘ 𝑎 ) ∈ ( 𝐶 ‘ 𝑏 ) )
76 72 73 75 3imtr4g ⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ) → ( 𝑎 E 𝑏 → ( 𝐶 ‘ 𝑎 ) E ( 𝐶 ‘ 𝑏 ) ) )
77 76 ralrimivva ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → ∀ 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( 𝑎 E 𝑏 → ( 𝐶 ‘ 𝑎 ) E ( 𝐶 ‘ 𝑏 ) ) )
78 soisoi ⊢ ( ( ( E Or ω ∧ E Po 𝑆 ) ∧ ( 𝐶 : ω –onto→ 𝑆 ∧ ∀ 𝑎 ∈ ω ∀ 𝑏 ∈ ω ( 𝑎 E 𝑏 → ( 𝐶 ‘ 𝑎 ) E ( 𝐶 ‘ 𝑏 ) ) ) ) → 𝐶 Isom E , E ( ω , 𝑆 ) )
79 6 11 14 77 78 syl22anc ⊢ ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) → 𝐶 Isom E , E ( ω , 𝑆 ) )