Metamath Proof Explorer


Theorem cantnf

Description: The Cantor Normal Form theorem. The function ( A CNF B ) , which maps a finitely supported function from B to A to the sum ( ( A ^o f ( a 1 ) ) o. a 1 ) +o ( ( A ^o f ( a 2 ) ) o. a 2 ) +o ... over all indices a < B such that f ( a ) is nonzero, is an order isomorphism from the ordering T of finitely supported functions to the set ( A ^o B ) under the natural order. Setting A = _om and letting B be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres , implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ( 𝜑𝐴 ∈ On )
cantnfs.b ( 𝜑𝐵 ∈ On )
oemapval.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
Assertion cantnf ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ( 𝜑𝐴 ∈ On )
3 cantnfs.b ( 𝜑𝐵 ∈ On )
4 oemapval.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
5 1 2 3 4 oemapso ( 𝜑𝑇 Or 𝑆 )
6 oecl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴o 𝐵 ) ∈ On )
7 2 3 6 syl2anc ( 𝜑 → ( 𝐴o 𝐵 ) ∈ On )
8 eloni ( ( 𝐴o 𝐵 ) ∈ On → Ord ( 𝐴o 𝐵 ) )
9 7 8 syl ( 𝜑 → Ord ( 𝐴o 𝐵 ) )
10 ordwe ( Ord ( 𝐴o 𝐵 ) → E We ( 𝐴o 𝐵 ) )
11 weso ( E We ( 𝐴o 𝐵 ) → E Or ( 𝐴o 𝐵 ) )
12 sopo ( E Or ( 𝐴o 𝐵 ) → E Po ( 𝐴o 𝐵 ) )
13 9 10 11 12 4syl ( 𝜑 → E Po ( 𝐴o 𝐵 ) )
14 1 2 3 cantnff ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴o 𝐵 ) )
15 14 frnd ( 𝜑 → ran ( 𝐴 CNF 𝐵 ) ⊆ ( 𝐴o 𝐵 ) )
16 onss ( ( 𝐴o 𝐵 ) ∈ On → ( 𝐴o 𝐵 ) ⊆ On )
17 7 16 syl ( 𝜑 → ( 𝐴o 𝐵 ) ⊆ On )
18 17 sseld ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ On ) )
19 eleq1w ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) ↔ 𝑦 ∈ ( 𝐴o 𝐵 ) ) )
20 eleq1w ( 𝑡 = 𝑦 → ( 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
21 19 20 imbi12d ( 𝑡 = 𝑦 → ( ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
22 21 imbi2d ( 𝑡 = 𝑦 → ( ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) )
23 r19.21v ( ∀ 𝑦𝑡 ( 𝜑 → ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ↔ ( 𝜑 → ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
24 ordelss ( ( Ord ( 𝐴o 𝐵 ) ∧ 𝑡 ∈ ( 𝐴o 𝐵 ) ) → 𝑡 ⊆ ( 𝐴o 𝐵 ) )
25 9 24 sylan ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) → 𝑡 ⊆ ( 𝐴o 𝐵 ) )
26 25 sselda ( ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) ∧ 𝑦𝑡 ) → 𝑦 ∈ ( 𝐴o 𝐵 ) )
27 pm5.5 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → ( ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
28 26 27 syl ( ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) ∧ 𝑦𝑡 ) → ( ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
29 28 ralbidva ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) → ( ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ ∀ 𝑦𝑡 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
30 dfss3 ( 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ↔ ∀ 𝑦𝑡 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) )
31 29 30 bitr4di ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) → ( ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ↔ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) )
32 eleq1 ( 𝑡 = ∅ → ( 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ↔ ∅ ∈ ran ( 𝐴 CNF 𝐵 ) ) )
33 2 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝐴 ∈ On )
34 33 adantr ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝐴 ∈ On )
35 3 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝐵 ∈ On )
36 35 adantr ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝐵 ∈ On )
37 simplrl ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ∈ ( 𝐴o 𝐵 ) )
38 simplrr ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) )
39 7 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴o 𝐵 ) ∈ On )
40 simprl ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ ( 𝐴o 𝐵 ) )
41 onelon ( ( ( 𝐴o 𝐵 ) ∈ On ∧ 𝑡 ∈ ( 𝐴o 𝐵 ) ) → 𝑡 ∈ On )
42 39 40 41 syl2anc ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ On )
43 on0eln0 ( 𝑡 ∈ On → ( ∅ ∈ 𝑡𝑡 ≠ ∅ ) )
44 42 43 syl ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ∅ ∈ 𝑡𝑡 ≠ ∅ ) )
45 44 biimpar ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → ∅ ∈ 𝑡 )
46 eqid { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } = { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) }
47 eqid ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) = ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) )
48 eqid ( 1st ‘ ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) = ( 1st ‘ ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) )
49 eqid ( 2nd ‘ ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) ) = ( 2nd ‘ ( ℩ 𝑑𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴o { 𝑐 ∈ On ∣ 𝑡 ∈ ( 𝐴o 𝑐 ) } ) ·o 𝑎 ) +o 𝑏 ) = 𝑡 ) ) )
50 1 34 36 4 37 38 45 46 47 48 49 cantnflem4 ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑡 ≠ ∅ ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) )
51 fczsupp0 ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅
52 51 eqcomi ∅ = ( ( 𝐵 × { ∅ } ) supp ∅ )
53 oieq2 ( ∅ = ( ( 𝐵 × { ∅ } ) supp ∅ ) → OrdIso ( E , ∅ ) = OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) ) )
54 52 53 ax-mp OrdIso ( E , ∅ ) = OrdIso ( E , ( ( 𝐵 × { ∅ } ) supp ∅ ) )
55 ne0i ( 𝑡 ∈ ( 𝐴o 𝐵 ) → ( 𝐴o 𝐵 ) ≠ ∅ )
56 55 ad2antrl ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴o 𝐵 ) ≠ ∅ )
57 oveq1 ( 𝐴 = ∅ → ( 𝐴o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
58 57 neeq1d ( 𝐴 = ∅ → ( ( 𝐴o 𝐵 ) ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) ≠ ∅ ) )
59 56 58 syl5ibcom ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 = ∅ → ( ∅ ↑o 𝐵 ) ≠ ∅ ) )
60 59 necon2d ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( ∅ ↑o 𝐵 ) = ∅ → 𝐴 ≠ ∅ ) )
61 on0eln0 ( 𝐵 ∈ On → ( ∅ ∈ 𝐵𝐵 ≠ ∅ ) )
62 oe0m1 ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
63 61 62 bitr3d ( 𝐵 ∈ On → ( 𝐵 ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
64 35 63 syl ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 ≠ ∅ ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
65 on0eln0 ( 𝐴 ∈ On → ( ∅ ∈ 𝐴𝐴 ≠ ∅ ) )
66 33 65 syl ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ∅ ∈ 𝐴𝐴 ≠ ∅ ) )
67 60 64 66 3imtr4d ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 ≠ ∅ → ∅ ∈ 𝐴 ) )
68 ne0i ( 𝑦𝐵𝐵 ≠ ∅ )
69 67 68 impel ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝑦𝐵 ) → ∅ ∈ 𝐴 )
70 fconstmpt ( 𝐵 × { ∅ } ) = ( 𝑦𝐵 ↦ ∅ )
71 69 70 fmptd ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) : 𝐵𝐴 )
72 0ex ∅ ∈ V
73 72 a1i ( 𝜑 → ∅ ∈ V )
74 3 73 fczfsuppd ( 𝜑 → ( 𝐵 × { ∅ } ) finSupp ∅ )
75 74 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) finSupp ∅ )
76 1 2 3 cantnfs ( 𝜑 → ( ( 𝐵 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝐵 × { ∅ } ) : 𝐵𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) )
77 76 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐵 × { ∅ } ) ∈ 𝑆 ↔ ( ( 𝐵 × { ∅ } ) : 𝐵𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) )
78 71 75 77 mpbir2and ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 × { ∅ } ) ∈ 𝑆 )
79 eqid seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
80 1 33 35 54 78 79 cantnfval ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) )
81 we0 E We ∅
82 eqid OrdIso ( E , ∅ ) = OrdIso ( E , ∅ )
83 82 oien ( ( ∅ ∈ V ∧ E We ∅ ) → dom OrdIso ( E , ∅ ) ≈ ∅ )
84 72 81 83 mp2an dom OrdIso ( E , ∅ ) ≈ ∅
85 en0 ( dom OrdIso ( E , ∅ ) ≈ ∅ ↔ dom OrdIso ( E , ∅ ) = ∅ )
86 84 85 mpbi dom OrdIso ( E , ∅ ) = ∅
87 86 fveq2i ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ )
88 79 seqom0g ( ∅ ∈ V → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
89 72 88 ax-mp ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅
90 87 89 eqtri ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ·o ( ( 𝐵 × { ∅ } ) ‘ ( OrdIso ( E , ∅ ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ∅ ) ) = ∅
91 80 90 eqtrdi ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )
92 14 adantr ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴o 𝐵 ) )
93 92 ffnd ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐴 CNF 𝐵 ) Fn 𝑆 )
94 fnfvelrn ( ( ( 𝐴 CNF 𝐵 ) Fn 𝑆 ∧ ( 𝐵 × { ∅ } ) ∈ 𝑆 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ∈ ran ( 𝐴 CNF 𝐵 ) )
95 93 78 94 syl2anc ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ∈ ran ( 𝐴 CNF 𝐵 ) )
96 91 95 eqeltrrd ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → ∅ ∈ ran ( 𝐴 CNF 𝐵 ) )
97 32 50 96 pm2.61ne ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝐴o 𝐵 ) ∧ 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) )
98 97 expr ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) → ( 𝑡 ⊆ ran ( 𝐴 CNF 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
99 31 98 sylbid ( ( 𝜑𝑡 ∈ ( 𝐴o 𝐵 ) ) → ( ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
100 99 ex ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → ( ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
101 100 com23 ( 𝜑 → ( ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
102 101 a2i ( ( 𝜑 → ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
103 102 a1i ( 𝑡 ∈ On → ( ( 𝜑 → ∀ 𝑦𝑡 ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) )
104 23 103 syl5bi ( 𝑡 ∈ On → ( ∀ 𝑦𝑡 ( 𝜑 → ( 𝑦 ∈ ( 𝐴o 𝐵 ) → 𝑦 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) → ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) ) )
105 22 104 tfis2 ( 𝑡 ∈ On → ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
106 105 com3l ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → ( 𝑡 ∈ On → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) ) )
107 18 106 mpdd ( 𝜑 → ( 𝑡 ∈ ( 𝐴o 𝐵 ) → 𝑡 ∈ ran ( 𝐴 CNF 𝐵 ) ) )
108 107 ssrdv ( 𝜑 → ( 𝐴o 𝐵 ) ⊆ ran ( 𝐴 CNF 𝐵 ) )
109 15 108 eqssd ( 𝜑 → ran ( 𝐴 CNF 𝐵 ) = ( 𝐴o 𝐵 ) )
110 dffo2 ( ( 𝐴 CNF 𝐵 ) : 𝑆onto→ ( 𝐴o 𝐵 ) ↔ ( ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴o 𝐵 ) ∧ ran ( 𝐴 CNF 𝐵 ) = ( 𝐴o 𝐵 ) ) )
111 14 109 110 sylanbrc ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆onto→ ( 𝐴o 𝐵 ) )
112 2 adantr ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝐴 ∈ On )
113 3 adantr ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝐵 ∈ On )
114 fveq2 ( 𝑧 = 𝑡 → ( 𝑥𝑧 ) = ( 𝑥𝑡 ) )
115 fveq2 ( 𝑧 = 𝑡 → ( 𝑦𝑧 ) = ( 𝑦𝑡 ) )
116 114 115 eleq12d ( 𝑧 = 𝑡 → ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ↔ ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ) )
117 eleq1w ( 𝑧 = 𝑡 → ( 𝑧𝑤𝑡𝑤 ) )
118 117 imbi1d ( 𝑧 = 𝑡 → ( ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
119 118 ralbidv ( 𝑧 = 𝑡 → ( ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
120 116 119 anbi12d ( 𝑧 = 𝑡 → ( ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ) )
121 120 cbvrexvw ( ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑡𝐵 ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
122 fveq1 ( 𝑥 = 𝑢 → ( 𝑥𝑡 ) = ( 𝑢𝑡 ) )
123 fveq1 ( 𝑦 = 𝑣 → ( 𝑦𝑡 ) = ( 𝑣𝑡 ) )
124 eleq12 ( ( ( 𝑥𝑡 ) = ( 𝑢𝑡 ) ∧ ( 𝑦𝑡 ) = ( 𝑣𝑡 ) ) → ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ↔ ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ) )
125 122 123 124 syl2an ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ↔ ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ) )
126 fveq1 ( 𝑥 = 𝑢 → ( 𝑥𝑤 ) = ( 𝑢𝑤 ) )
127 fveq1 ( 𝑦 = 𝑣 → ( 𝑦𝑤 ) = ( 𝑣𝑤 ) )
128 126 127 eqeqan12d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ↔ ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) )
129 128 imbi2d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) )
130 129 ralbidv ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) )
131 125 130 anbi12d ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ( ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) ) )
132 131 rexbidv ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ∃ 𝑡𝐵 ( ( 𝑥𝑡 ) ∈ ( 𝑦𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑡𝐵 ( ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) ) )
133 121 132 syl5bb ( ( 𝑥 = 𝑢𝑦 = 𝑣 ) → ( ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑡𝐵 ( ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) ) )
134 133 cbvopabv { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑡𝐵 ( ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) }
135 4 134 eqtri 𝑇 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∃ 𝑡𝐵 ( ( 𝑢𝑡 ) ∈ ( 𝑣𝑡 ) ∧ ∀ 𝑤𝐵 ( 𝑡𝑤 → ( 𝑢𝑤 ) = ( 𝑣𝑤 ) ) ) }
136 simprll ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑓𝑆 )
137 simprlr ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑔𝑆 )
138 simprr ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → 𝑓 𝑇 𝑔 )
139 eqid { 𝑐𝐵 ∣ ( 𝑓𝑐 ) ∈ ( 𝑔𝑐 ) } = { 𝑐𝐵 ∣ ( 𝑓𝑐 ) ∈ ( 𝑔𝑐 ) }
140 eqid OrdIso ( E , ( 𝑔 supp ∅ ) ) = OrdIso ( E , ( 𝑔 supp ∅ ) )
141 eqid seqω ( ( 𝑘 ∈ V , 𝑡 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑔 ‘ ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑡 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑡 ∈ V ↦ ( ( ( 𝐴o ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑔 ‘ ( OrdIso ( E , ( 𝑔 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑡 ) ) , ∅ )
142 1 112 113 135 136 137 138 139 140 141 cantnflem1 ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) )
143 fvex ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ∈ V
144 143 epeli ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) )
145 142 144 sylibr ( ( 𝜑 ∧ ( ( 𝑓𝑆𝑔𝑆 ) ∧ 𝑓 𝑇 𝑔 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) )
146 145 expr ( ( 𝜑 ∧ ( 𝑓𝑆𝑔𝑆 ) ) → ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) )
147 146 ralrimivva ( 𝜑 → ∀ 𝑓𝑆𝑔𝑆 ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) )
148 soisoi ( ( ( 𝑇 Or 𝑆 ∧ E Po ( 𝐴o 𝐵 ) ) ∧ ( ( 𝐴 CNF 𝐵 ) : 𝑆onto→ ( 𝐴o 𝐵 ) ∧ ∀ 𝑓𝑆𝑔𝑆 ( 𝑓 𝑇 𝑔 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑓 ) E ( ( 𝐴 CNF 𝐵 ) ‘ 𝑔 ) ) ) ) → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴o 𝐵 ) ) )
149 5 13 111 147 148 syl22anc ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴o 𝐵 ) ) )