Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnf Structured version   Visualization version   GIF version

Theorem cantnf 9155
 Description: The Cantor Normal Form theorem. The function (𝐴 CNF 𝐵), which maps a finitely supported function from 𝐵 to 𝐴 to the sum ((𝐴 ↑o 𝑓(𝑎1)) ∘ 𝑎1) +o ((𝐴 ↑o 𝑓(𝑎2)) ∘ 𝑎2) +o ... over all indices 𝑎 < 𝐵 such that 𝑓(𝑎) is nonzero, is an order isomorphism from the ordering 𝑇 of finitely supported functions to the set (𝐴 ↑o 𝐵) under the natural order. Setting 𝐴 = ω and letting 𝐵 be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres 9139, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
oemapval.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
Assertion
Ref Expression
cantnf (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴o 𝐵)))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐵   𝑤,𝐴,𝑥,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑤)   𝑆(𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cantnf
Dummy variables 𝑓 𝑐 𝑔 𝑘 𝑡 𝑢 𝑣 𝑎 𝑏 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . 3 𝑆 = dom (𝐴 CNF 𝐵)
2 cantnfs.a . . 3 (𝜑𝐴 ∈ On)
3 cantnfs.b . . 3 (𝜑𝐵 ∈ On)
4 oemapval.t . . 3 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
51, 2, 3, 4oemapso 9144 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 8160 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
72, 3, 6syl2anc 587 . . . 4 (𝜑 → (𝐴o 𝐵) ∈ On)
8 eloni 6190 . . . 4 ((𝐴o 𝐵) ∈ On → Ord (𝐴o 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴o 𝐵))
10 ordwe 6193 . . 3 (Ord (𝐴o 𝐵) → E We (𝐴o 𝐵))
11 weso 5534 . . 3 ( E We (𝐴o 𝐵) → E Or (𝐴o 𝐵))
12 sopo 5480 . . 3 ( E Or (𝐴o 𝐵) → E Po (𝐴o 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴o 𝐵))
141, 2, 3cantnff 9136 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
1514frnd 6512 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴o 𝐵))
16 onss 7501 . . . . . . . 8 ((𝐴o 𝐵) ∈ On → (𝐴o 𝐵) ⊆ On)
177, 16syl 17 . . . . . . 7 (𝜑 → (𝐴o 𝐵) ⊆ On)
1817sseld 3952 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ On))
19 eleq1w 2898 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴o 𝐵) ↔ 𝑦 ∈ (𝐴o 𝐵)))
20 eleq1w 2898 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2119, 20imbi12d 348 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2221imbi2d 344 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
23 r19.21v 3170 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
24 ordelss 6196 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴o 𝐵) ∧ 𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ⊆ (𝐴o 𝐵))
259, 24sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ⊆ (𝐴o 𝐵))
2625sselda 3953 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴o 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴o 𝐵))
27 pm5.5 365 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴o 𝐵) → ((𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2826, 27syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴o 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2928ralbidva 3191 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
30 dfss3 3941 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3129, 30syl6bbr 292 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
32 eleq1 2903 . . . . . . . . . . . . . . . 16 (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵)))
332adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On)
3433adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On)
353adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On)
3635adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On)
37 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴o 𝐵))
38 simplrr 777 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
397adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴o 𝐵) ∈ On)
40 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴o 𝐵))
41 onelon 6205 . . . . . . . . . . . . . . . . . . . 20 (((𝐴o 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ∈ On)
4239, 40, 41syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
43 on0eln0 6235 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ On → (∅ ∈ 𝑡𝑡 ≠ ∅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡𝑡 ≠ ∅))
4544biimpar 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡)
46 eqid 2824 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)} = {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}
47 eqid 2824 . . . . . . . . . . . . . . . . 17 (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)) = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))
48 eqid 2824 . . . . . . . . . . . . . . . . 17 (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))) = (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)))
49 eqid 2824 . . . . . . . . . . . . . . . . 17 (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))) = (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)))
501, 34, 36, 4, 37, 38, 45, 46, 47, 48, 49cantnflem4 9154 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
51 fczsupp0 7857 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5251eqcomi 2833 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
53 oieq2 8976 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
55 ne0i 4283 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 ∈ (𝐴o 𝐵) → (𝐴o 𝐵) ≠ ∅)
5655ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴o 𝐵) ≠ ∅)
57 oveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → (𝐴o 𝐵) = (∅ ↑o 𝐵))
5857neeq1d 3073 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 = ∅ → ((𝐴o 𝐵) ≠ ∅ ↔ (∅ ↑o 𝐵) ≠ ∅))
5956, 58syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑o 𝐵) ≠ ∅))
6059necon2d 3037 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑o 𝐵) = ∅ → 𝐴 ≠ ∅))
61 on0eln0 6235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
62 oe0m1 8144 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
6361, 62bitr3d 284 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑o 𝐵) = ∅))
6435, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑o 𝐵) = ∅))
65 on0eln0 6235 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
6633, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴𝐴 ≠ ∅))
6760, 64, 663imtr4d 297 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴))
68 ne0i 4283 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵𝐵 ≠ ∅)
6967, 68impel 509 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦𝐵) → ∅ ∈ 𝐴)
70 fconstmpt 5602 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7169, 70fmptd 6871 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
72 0ex 5198 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
743, 73fczfsuppd 8850 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7574adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
761, 2, 3cantnfs 9128 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7776adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7871, 75, 77mpbir2and 712 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆)
79 eqid 2824 . . . . . . . . . . . . . . . . . . 19 seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)
801, 33, 35, 54, 78, 79cantnfval 9130 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅)))
81 we0 5538 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
82 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8382oien 9001 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8472, 81, 83mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
85 en0 8570 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8684, 85mpbi 233 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8786fveq2i 6666 . . . . . . . . . . . . . . . . . . 19 (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅)) = (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘∅)
8879seqom0g 8090 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ V → (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘∅) = ∅)
8972, 88ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘∅) = ∅
9087, 89eqtri 2847 . . . . . . . . . . . . . . . . . 18 (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅)) = ∅
9180, 90syl6eq 2875 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
9214adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
9392ffnd 6506 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
94 fnfvelrn 6841 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9593, 78, 94syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9691, 95eqeltrrd 2917 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
9732, 50, 96pm2.61ne 3099 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
9897expr 460 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
9931, 98sylbid 243 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
10099ex 416 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
101100com23 86 . . . . . . . . . . 11 (𝜑 → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
102101a2i 14 . . . . . . . . . 10 ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
103102a1i 11 . . . . . . . . 9 (𝑡 ∈ On → ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10423, 103syl5bi 245 . . . . . . . 8 (𝑡 ∈ On → (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10522, 104tfis2 7567 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
106105com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
10718, 106mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
108107ssrdv 3959 . . . 4 (𝜑 → (𝐴o 𝐵) ⊆ ran (𝐴 CNF 𝐵))
10915, 108eqssd 3970 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴o 𝐵))
110 dffo2 6587 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴o 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴o 𝐵)))
11114, 109, 110sylanbrc 586 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴o 𝐵))
1122adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1133adantr 484 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
114 fveq2 6663 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
115 fveq2 6663 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
116114, 115eleq12d 2910 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
117 eleq1w 2898 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
118117imbi1d 345 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
119118ralbidv 3192 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
120116, 119anbi12d 633 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
121120cbvrexvw 3435 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
122 fveq1 6662 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
123 fveq1 6662 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
124 eleq12 2905 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
125122, 123, 124syl2an 598 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
126 fveq1 6662 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
127 fveq1 6662 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
128126, 127eqeqan12d 2841 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
129128imbi2d 344 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
130129ralbidv 3192 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
131125, 130anbi12d 633 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
132131rexbidv 3289 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
133121, 132syl5bb 286 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
134133cbvopabv 5125 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1354, 134eqtri 2847 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
136 simprll 778 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
137 simprlr 779 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
138 simprr 772 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔)
139 eqid 2824 . . . . . 6 {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)} = {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)}
140 eqid 2824 . . . . . 6 OrdIso( E , (𝑔 supp ∅)) = OrdIso( E , (𝑔 supp ∅))
141 eqid 2824 . . . . . 6 seqω((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴o (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·o (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +o 𝑡)), ∅) = seqω((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴o (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·o (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +o 𝑡)), ∅)
1421, 112, 113, 135, 136, 137, 138, 139, 140, 141cantnflem1 9151 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
143 fvex 6676 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
144143epeli 5456 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
145142, 144sylibr 237 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
146145expr 460 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
147146ralrimivva 3186 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
148 soisoi 7076 . 2 (((𝑇 Or 𝑆 ∧ E Po (𝐴o 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆onto→(𝐴o 𝐵) ∧ ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴o 𝐵)))
1495, 13, 111, 147, 148syl22anc 837 1 (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴o 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  {crab 3137  Vcvv 3480   ⊆ wss 3919  ∅c0 4276  {csn 4550  ⟨cop 4556  ∪ cuni 4824  ∩ cint 4862   class class class wbr 5053  {copab 5115   E cep 5452   Po wpo 5460   Or wor 5461   We wwe 5501   × cxp 5541  dom cdm 5543  ran crn 5544  Ord word 6179  Oncon0 6180  ℩cio 6302   Fn wfn 6340  ⟶wf 6341  –onto→wfo 6343  ‘cfv 6345   Isom wiso 6346  (class class class)co 7151   ∈ cmpo 7153  1st c1st 7684  2nd c2nd 7685   supp csupp 7828  seqωcseqom 8081   +o coa 8097   ·o comu 8098   ↑o coe 8099   ≈ cen 8504   finSupp cfsupp 8832  OrdIsocoi 8972   CNF ccnf 9123 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-seqom 8082  df-1o 8100  df-2o 8101  df-oadd 8104  df-omul 8105  df-oexp 8106  df-er 8287  df-map 8406  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-oi 8973  df-cnf 9124 This theorem is referenced by:  oemapwe  9156  cantnffval2  9157  cantnff1o  9158
 Copyright terms: Public domain W3C validator