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

Theorem cantnf 8833
Description: The Cantor Normal Form theorem. The function (𝐴 CNF 𝐵), which maps a finitely supported function from 𝐵 to 𝐴 to the sum ((𝐴𝑜 𝑓(𝑎1)) ∘ 𝑎1) +𝑜 ((𝐴𝑜 𝑓(𝑎2)) ∘ 𝑎2) +𝑜 ... over all indices 𝑎 < 𝐵 such that 𝑓(𝑎) is nonzero, is an order isomorphism from the ordering 𝑇 of finitely supported functions to the set (𝐴𝑜 𝐵) 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 8817, 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 (𝑆, (𝐴𝑜 𝐵)))
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 8822 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 7850 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
72, 3, 6syl2anc 575 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ∈ On)
8 eloni 5946 . . . 4 ((𝐴𝑜 𝐵) ∈ On → Ord (𝐴𝑜 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴𝑜 𝐵))
10 ordwe 5949 . . 3 (Ord (𝐴𝑜 𝐵) → E We (𝐴𝑜 𝐵))
11 weso 5302 . . 3 ( E We (𝐴𝑜 𝐵) → E Or (𝐴𝑜 𝐵))
12 sopo 5249 . . 3 ( E Or (𝐴𝑜 𝐵) → E Po (𝐴𝑜 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴𝑜 𝐵))
141, 2, 3cantnff 8814 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
1514frnd 6259 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
16 onss 7216 . . . . . . . 8 ((𝐴𝑜 𝐵) ∈ On → (𝐴𝑜 𝐵) ⊆ On)
177, 16syl 17 . . . . . . 7 (𝜑 → (𝐴𝑜 𝐵) ⊆ On)
1817sseld 3797 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ On))
19 eleq1w 2868 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴𝑜 𝐵) ↔ 𝑦 ∈ (𝐴𝑜 𝐵)))
20 eleq1w 2868 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2119, 20imbi12d 335 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2221imbi2d 331 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
23 r19.21v 3148 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
24 ordelss 5952 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴𝑜 𝐵) ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
259, 24sylan 571 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
2625sselda 3798 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴𝑜 𝐵))
27 pm5.5 352 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝑜 𝐵) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2826, 27syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2928ralbidva 3173 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
30 dfss3 3787 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3129, 30syl6bbr 280 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
32 eleq1 2873 . . . . . . . . . . . . . . . 16 (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵)))
332adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On)
3433adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On)
353adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On)
3635adantr 468 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On)
37 simplrl 786 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴𝑜 𝐵))
38 simplrr 787 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
397adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ∈ On)
40 simprl 778 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴𝑜 𝐵))
41 onelon 5961 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑜 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ∈ On)
4239, 40, 41syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
43 on0eln0 5992 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ On → (∅ ∈ 𝑡𝑡 ≠ ∅))
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡𝑡 ≠ ∅))
4544biimpar 465 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡)
46 eqid 2806 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)} = {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}
47 eqid 2806 . . . . . . . . . . . . . . . . 17 (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)) = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))
48 eqid 2806 . . . . . . . . . . . . . . . . 17 (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
49 eqid 2806 . . . . . . . . . . . . . . . . 17 (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
501, 34, 36, 4, 37, 38, 45, 46, 47, 48, 49cantnflem4 8832 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
51 fczsupp0 7555 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5251eqcomi 2815 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
53 oieq2 8653 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
55 ne0i 4122 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵𝐵 ≠ ∅)
56 ne0i 4122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ (𝐴𝑜 𝐵) → (𝐴𝑜 𝐵) ≠ ∅)
5756ad2antrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ≠ ∅)
58 oveq1 6877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
5958neeq1d 3037 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ≠ ∅ ↔ (∅ ↑𝑜 𝐵) ≠ ∅))
6057, 59syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑𝑜 𝐵) ≠ ∅))
6160necon2d 3001 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅))
62 on0eln0 5992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
63 oe0m1 7834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
6462, 63bitr3d 272 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
6535, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
66 on0eln0 5992 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
6733, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴𝐴 ≠ ∅))
6861, 65, 673imtr4d 285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴))
6955, 68syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝑦𝐵 → ∅ ∈ 𝐴))
7069imp 395 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦𝐵) → ∅ ∈ 𝐴)
71 fconstmpt 5363 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7270, 71fmptd 6602 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
73 0ex 4984 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7473a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
753, 74fczfsuppd 8528 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7675adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
771, 2, 3cantnfs 8806 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7877adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7972, 76, 78mpbir2and 695 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆)
80 eqid 2806 . . . . . . . . . . . . . . . . . . 19 seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)
811, 33, 35, 54, 79, 80cantnfval 8808 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)))
82 we0 5306 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
83 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8483oien 8678 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8573, 82, 84mp2an 675 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
86 en0 8251 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8785, 86mpbi 221 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8887fveq2i 6407 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅)
8980seqom0g 7783 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ V → (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅)
9073, 89ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅
9188, 90eqtri 2828 . . . . . . . . . . . . . . . . . 18 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = ∅
9281, 91syl6eq 2856 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
9314adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
9493ffnd 6253 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
95 fnfvelrn 6574 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9694, 79, 95syl2anc 575 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9792, 96eqeltrrd 2886 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
9832, 50, 97pm2.61ne 3063 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
9998expr 446 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
10031, 99sylbid 231 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
101100ex 399 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
102101com23 86 . . . . . . . . . . 11 (𝜑 → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
103102a2i 14 . . . . . . . . . 10 ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
104103a1i 11 . . . . . . . . 9 (𝑡 ∈ On → ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10523, 104syl5bi 233 . . . . . . . 8 (𝑡 ∈ On → (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10622, 105tfis2 7282 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
107106com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
10818, 107mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
109108ssrdv 3804 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵))
11015, 109eqssd 3815 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵))
111 dffo2 6331 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵)))
11214, 110, 111sylanbrc 574 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵))
1132adantr 468 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1143adantr 468 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
115 fveq2 6404 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
116 fveq2 6404 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
117115, 116eleq12d 2879 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
118 eleq1w 2868 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
119118imbi1d 332 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
120119ralbidv 3174 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
121117, 120anbi12d 618 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
122121cbvrexv 3361 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
123 fveq1 6403 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
124 fveq1 6403 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
125 eleq12 2875 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
126123, 124, 125syl2an 585 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
127 fveq1 6403 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
128 fveq1 6403 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
129127, 128eqeqan12d 2822 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
130129imbi2d 331 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
131130ralbidv 3174 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
132126, 131anbi12d 618 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
133132rexbidv 3240 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
134122, 133syl5bb 274 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
135134cbvopabv 4916 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1364, 135eqtri 2828 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
137 simprll 788 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
138 simprlr 789 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
139 simprr 780 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔)
140 eqid 2806 . . . . . 6 {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)} = {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)}
141 eqid 2806 . . . . . 6 OrdIso( E , (𝑔 supp ∅)) = OrdIso( E , (𝑔 supp ∅))
142 eqid 2806 . . . . . 6 seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅) = seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅)
1431, 113, 114, 136, 137, 138, 139, 140, 141, 142cantnflem1 8829 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
144 fvex 6417 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
145144epeli 5226 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
146143, 145sylibr 225 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
147146expr 446 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
148147ralrimivva 3159 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
149 soisoi 6798 . 2 (((𝑇 Or 𝑆 ∧ E Po (𝐴𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ∧ ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
1505, 13, 112, 148, 149syl22anc 858 1 (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  wss 3769  c0 4116  {csn 4370  cop 4376   cuni 4630   cint 4669   class class class wbr 4844  {copab 4906   E cep 5223   Po wpo 5230   Or wor 5231   We wwe 5269   × cxp 5309  dom cdm 5311  ran crn 5312  Ord word 5935  Oncon0 5936  cio 6058   Fn wfn 6092  wf 6093  ontowfo 6095  cfv 6097   Isom wiso 6098  (class class class)co 6870  cmpt2 6872  1st c1st 7392  2nd c2nd 7393   supp csupp 7525  seq𝜔cseqom 7774   +𝑜 coa 7789   ·𝑜 comu 7790  𝑜 coe 7791  cen 8185   finSupp cfsupp 8510  OrdIsocoi 8649   CNF ccnf 8801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-seqom 7775  df-1o 7792  df-2o 7793  df-oadd 7796  df-omul 7797  df-oexp 7798  df-er 7975  df-map 8090  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-oi 8650  df-cnf 8802
This theorem is referenced by:  oemapwe  8834  cantnffval2  8835  cantnff1o  8836
  Copyright terms: Public domain W3C validator