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

Theorem cantnf 9629
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 9613, 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 9618 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 8483 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
72, 3, 6syl2anc 584 . . . 4 (𝜑 → (𝐴o 𝐵) ∈ On)
8 eloni 6327 . . . 4 ((𝐴o 𝐵) ∈ On → Ord (𝐴o 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴o 𝐵))
10 ordwe 6330 . . 3 (Ord (𝐴o 𝐵) → E We (𝐴o 𝐵))
11 weso 5624 . . 3 ( E We (𝐴o 𝐵) → E Or (𝐴o 𝐵))
12 sopo 5564 . . 3 ( E Or (𝐴o 𝐵) → E Po (𝐴o 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴o 𝐵))
141, 2, 3cantnff 9610 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
1514frnd 6676 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴o 𝐵))
16 onss 7719 . . . . . . . 8 ((𝐴o 𝐵) ∈ On → (𝐴o 𝐵) ⊆ On)
177, 16syl 17 . . . . . . 7 (𝜑 → (𝐴o 𝐵) ⊆ On)
1817sseld 3943 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ On))
19 eleq1w 2820 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴o 𝐵) ↔ 𝑦 ∈ (𝐴o 𝐵)))
20 eleq1w 2820 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2119, 20imbi12d 344 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2221imbi2d 340 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
23 r19.21v 3176 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
24 ordelss 6333 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴o 𝐵) ∧ 𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ⊆ (𝐴o 𝐵))
259, 24sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ⊆ (𝐴o 𝐵))
2625sselda 3944 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴o 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴o 𝐵))
27 pm5.5 361 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴o 𝐵) → ((𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2826, 27syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴o 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2928ralbidva 3172 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
30 dfss3 3932 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3129, 30bitr4di 288 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
32 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵)))
332adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On)
3433adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On)
353adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On)
3635adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On)
37 simplrl 775 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴o 𝐵))
38 simplrr 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
397adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴o 𝐵) ∈ On)
40 simprl 769 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴o 𝐵))
41 onelon 6342 . . . . . . . . . . . . . . . . . . . 20 (((𝐴o 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴o 𝐵)) → 𝑡 ∈ On)
4239, 40, 41syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
43 on0eln0 6373 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ On → (∅ ∈ 𝑡𝑡 ≠ ∅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡𝑡 ≠ ∅))
4544biimpar 478 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡)
46 eqid 2736 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)} = {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}
47 eqid 2736 . . . . . . . . . . . . . . . . 17 (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)) = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))
48 eqid 2736 . . . . . . . . . . . . . . . . 17 (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡))) = (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴o 𝑐)}) ·o 𝑎) +o 𝑏) = 𝑡)))
49 eqid 2736 . . . . . . . . . . . . . . . . 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 9628 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
51 fczsupp0 8124 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5251eqcomi 2745 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
53 oieq2 9449 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
55 ne0i 4294 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 ∈ (𝐴o 𝐵) → (𝐴o 𝐵) ≠ ∅)
5655ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴o 𝐵) ≠ ∅)
57 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → (𝐴o 𝐵) = (∅ ↑o 𝐵))
5857neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 = ∅ → ((𝐴o 𝐵) ≠ ∅ ↔ (∅ ↑o 𝐵) ≠ ∅))
5956, 58syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑o 𝐵) ≠ ∅))
6059necon2d 2966 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑o 𝐵) = ∅ → 𝐴 ≠ ∅))
61 on0eln0 6373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
62 oe0m1 8467 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
6361, 62bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑o 𝐵) = ∅))
6435, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑o 𝐵) = ∅))
65 on0eln0 6373 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
6633, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴𝐴 ≠ ∅))
6760, 64, 663imtr4d 293 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴))
68 ne0i 4294 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵𝐵 ≠ ∅)
6967, 68impel 506 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦𝐵) → ∅ ∈ 𝐴)
70 fconstmpt 5694 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7169, 70fmptd 7062 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
72 0ex 5264 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
743, 73fczfsuppd 9323 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7574adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
761, 2, 3cantnfs 9602 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7776adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7871, 75, 77mpbir2and 711 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆)
79 eqid 2736 . . . . . . . . . . . . . . . . . . 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 9604 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅)))
81 we0 5628 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
82 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8382oien 9474 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8472, 81, 83mp2an 690 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
85 en0 8957 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8684, 85mpbi 229 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8786fveq2i 6845 . . . . . . . . . . . . . . . . . . 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 8402 . . . . . . . . . . . . . . . . . . . 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 2764 . . . . . . . . . . . . . . . . . 18 (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , ∅)‘𝑘)) ·o ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , ∅)) = ∅
9180, 90eqtrdi 2792 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
9214adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
9392ffnd 6669 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
94 fnfvelrn 7031 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9593, 78, 94syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9691, 95eqeltrrd 2839 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
9732, 50, 96pm2.61ne 3030 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴o 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
9897expr 457 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
9931, 98sylbid 239 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴o 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
10099ex 413 . . . . . . . . . . . 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, 103biimtrid 241 . . . . . . . 8 (𝑡 ∈ On → (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴o 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10522, 104tfis2 7793 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
106105com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
10718, 106mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴o 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
108107ssrdv 3950 . . . 4 (𝜑 → (𝐴o 𝐵) ⊆ ran (𝐴 CNF 𝐵))
10915, 108eqssd 3961 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴o 𝐵))
110 dffo2 6760 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴o 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴o 𝐵)))
11114, 109, 110sylanbrc 583 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴o 𝐵))
1122adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1133adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
114 fveq2 6842 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
115 fveq2 6842 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
116114, 115eleq12d 2832 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
117 eleq1w 2820 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
118117imbi1d 341 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
119118ralbidv 3174 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
120116, 119anbi12d 631 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
121120cbvrexvw 3226 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
122 fveq1 6841 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
123 fveq1 6841 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
124 eleq12 2827 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
125122, 123, 124syl2an 596 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
126 fveq1 6841 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
127 fveq1 6841 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
128126, 127eqeqan12d 2750 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
129128imbi2d 340 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
130129ralbidv 3174 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
131125, 130anbi12d 631 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
132131rexbidv 3175 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
133121, 132bitrid 282 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
134133cbvopabv 5178 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1354, 134eqtri 2764 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
136 simprll 777 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
137 simprlr 778 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
138 simprr 771 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔)
139 eqid 2736 . . . . . 6 {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)} = {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)}
140 eqid 2736 . . . . . 6 OrdIso( E , (𝑔 supp ∅)) = OrdIso( E , (𝑔 supp ∅))
141 eqid 2736 . . . . . 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 9625 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
143 fvex 6855 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
144143epeli 5539 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
145142, 144sylibr 233 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
146145expr 457 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
147146ralrimivva 3197 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
148 soisoi 7273 . 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 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  c0 4282  {csn 4586  cop 4592   cuni 4865   cint 4907   class class class wbr 5105  {copab 5167   E cep 5536   Po wpo 5543   Or wor 5544   We wwe 5587   × cxp 5631  dom cdm 5633  ran crn 5634  Ord word 6316  Oncon0 6317  cio 6446   Fn wfn 6491  wf 6492  ontowfo 6494  cfv 6496   Isom wiso 6497  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920   supp csupp 8092  seqωcseqom 8393   +o coa 8409   ·o comu 8410  o coe 8411  cen 8880   finSupp cfsupp 9305  OrdIsocoi 9445   CNF ccnf 9597
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-seqom 8394  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-oexp 8418  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-cnf 9598
This theorem is referenced by:  oemapwe  9630  cantnffval2  9631  cantnff1o  9632  cantnfresb  41644
  Copyright terms: Public domain W3C validator