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 biimtrid ⊢ ( 𝑡 ∈ 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 bitrid ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑡 ∈ 𝐵 ( ( 𝑢 ‘ 𝑡 ) ∈ ( 𝑣 ‘ 𝑡 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑡 ∈ 𝑤 → ( 𝑢 ‘ 𝑤 ) = ( 𝑣 ‘ 𝑤 ) ) ) ) )
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 𝐵 ) ) )