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

Theorem cantnf 8587
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 indexes 𝑎 < 𝐵 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 8571, 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 8576 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 7614 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
72, 3, 6syl2anc 693 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ∈ On)
8 eloni 5731 . . . 4 ((𝐴𝑜 𝐵) ∈ On → Ord (𝐴𝑜 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴𝑜 𝐵))
10 ordwe 5734 . . 3 (Ord (𝐴𝑜 𝐵) → E We (𝐴𝑜 𝐵))
11 weso 5103 . . 3 ( E We (𝐴𝑜 𝐵) → E Or (𝐴𝑜 𝐵))
12 sopo 5050 . . 3 ( E Or (𝐴𝑜 𝐵) → E Po (𝐴𝑜 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴𝑜 𝐵))
141, 2, 3cantnff 8568 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
15 frn 6051 . . . . 5 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
1614, 15syl 17 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
17 onss 6987 . . . . . . . 8 ((𝐴𝑜 𝐵) ∈ On → (𝐴𝑜 𝐵) ⊆ On)
187, 17syl 17 . . . . . . 7 (𝜑 → (𝐴𝑜 𝐵) ⊆ On)
1918sseld 3600 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ On))
20 eleq1 2688 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴𝑜 𝐵) ↔ 𝑦 ∈ (𝐴𝑜 𝐵)))
21 eleq1 2688 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2220, 21imbi12d 334 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2322imbi2d 330 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
24 r19.21v 2959 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
25 ordelss 5737 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴𝑜 𝐵) ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
269, 25sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
2726sselda 3601 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴𝑜 𝐵))
28 pm5.5 351 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝑜 𝐵) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2927, 28syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
3029ralbidva 2984 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
31 dfss3 3590 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3230, 31syl6bbr 278 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
33 eleq1 2688 . . . . . . . . . . . . . . . 16 (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵)))
342adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On)
3534adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On)
363adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On)
3736adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On)
38 simplrl 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴𝑜 𝐵))
39 simplrr 801 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
407adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ∈ On)
41 simprl 794 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴𝑜 𝐵))
42 onelon 5746 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑜 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ∈ On)
4340, 41, 42syl2anc 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
44 on0eln0 5778 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ On → (∅ ∈ 𝑡𝑡 ≠ ∅))
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡𝑡 ≠ ∅))
4645biimpar 502 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡)
47 eqid 2621 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)} = {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}
48 eqid 2621 . . . . . . . . . . . . . . . . 17 (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)) = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))
49 eqid 2621 . . . . . . . . . . . . . . . . 17 (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
50 eqid 2621 . . . . . . . . . . . . . . . . 17 (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
511, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50cantnflem4 8586 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
52 fczsupp0 7321 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5352eqcomi 2630 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
54 oieq2 8415 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
56 ne0i 3919 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵𝐵 ≠ ∅)
57 ne0i 3919 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ (𝐴𝑜 𝐵) → (𝐴𝑜 𝐵) ≠ ∅)
5857ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ≠ ∅)
59 oveq1 6654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
6059neeq1d 2852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ≠ ∅ ↔ (∅ ↑𝑜 𝐵) ≠ ∅))
6158, 60syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑𝑜 𝐵) ≠ ∅))
6261necon2d 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅))
63 on0eln0 5778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
64 oe0m1 7598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
6563, 64bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
6636, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
67 on0eln0 5778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
6834, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴𝐴 ≠ ∅))
6962, 66, 683imtr4d 283 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴))
7056, 69syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝑦𝐵 → ∅ ∈ 𝐴))
7170imp 445 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦𝐵) → ∅ ∈ 𝐴)
72 fconstmpt 5161 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7371, 72fmptd 6383 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
74 0ex 4788 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
763, 75fczfsuppd 8290 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7776adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
781, 2, 3cantnfs 8560 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7978adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
8073, 77, 79mpbir2and 957 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆)
81 eqid 2621 . . . . . . . . . . . . . . . . . . 19 seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)
821, 34, 36, 55, 80, 81cantnfval 8562 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)))
83 we0 5107 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
84 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8584oien 8440 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8674, 83, 85mp2an 708 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
87 en0 8016 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8886, 87mpbi 220 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8988fveq2i 6192 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅)
9081seqom0g 7548 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ V → (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅)
9174, 90ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅
9289, 91eqtri 2643 . . . . . . . . . . . . . . . . . 18 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = ∅
9382, 92syl6eq 2671 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
9414adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
95 ffn 6043 . . . . . . . . . . . . . . . . . . 19 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆)
9694, 95syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
97 fnfvelrn 6354 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9896, 80, 97syl2anc 693 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9993, 98eqeltrrd 2701 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
10033, 51, 99pm2.61ne 2878 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
101100expr 643 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
10232, 101sylbid 230 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
103102ex 450 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
104103com23 86 . . . . . . . . . . 11 (𝜑 → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
105104a2i 14 . . . . . . . . . 10 ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
106105a1i 11 . . . . . . . . 9 (𝑡 ∈ On → ((𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10724, 106syl5bi 232 . . . . . . . 8 (𝑡 ∈ On → (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))))
10823, 107tfis2 7053 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
109108com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
11019, 109mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
111110ssrdv 3607 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵))
11216, 111eqssd 3618 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵))
113 dffo2 6117 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵)))
11414, 112, 113sylanbrc 698 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵))
1152adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1163adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
117 fveq2 6189 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
118 fveq2 6189 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
119117, 118eleq12d 2694 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
120 eleq1 2688 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
121120imbi1d 331 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
122121ralbidv 2985 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
123119, 122anbi12d 747 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
124123cbvrexv 3170 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
125 fveq1 6188 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
126 fveq1 6188 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
127 eleq12 2690 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
128125, 126, 127syl2an 494 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
129 fveq1 6188 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
130 fveq1 6188 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
131129, 130eqeqan12d 2637 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
132131imbi2d 330 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
133132ralbidv 2985 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
134128, 133anbi12d 747 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
135134rexbidv 3050 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
136124, 135syl5bb 272 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
137136cbvopabv 4720 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1384, 137eqtri 2643 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
139 simprll 802 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
140 simprlr 803 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
141 simprr 796 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔)
142 eqid 2621 . . . . . 6 {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)} = {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)}
143 eqid 2621 . . . . . 6 OrdIso( E , (𝑔 supp ∅)) = OrdIso( E , (𝑔 supp ∅))
144 eqid 2621 . . . . . 6 seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅) = seq𝜔((𝑘 ∈ V, 𝑡 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝑔 supp ∅))‘𝑘)) ·𝑜 (𝑔‘(OrdIso( E , (𝑔 supp ∅))‘𝑘))) +𝑜 𝑡)), ∅)
1451, 115, 116, 138, 139, 140, 141, 142, 143, 144cantnflem1 8583 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
146 fvex 6199 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
147146epelc 5029 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
148145, 147sylibr 224 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
149148expr 643 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
150149ralrimivva 2970 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
151 soisoi 6575 . 2 (((𝑇 Or 𝑆 ∧ E Po (𝐴𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ∧ ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
1525, 13, 114, 150, 151syl22anc 1326 1 (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1482  wcel 1989  wne 2793  wral 2911  wrex 2912  {crab 2915  Vcvv 3198  wss 3572  c0 3913  {csn 4175  cop 4181   cuni 4434   cint 4473   class class class wbr 4651  {copab 4710   E cep 5026   Po wpo 5031   Or wor 5032   We wwe 5070   × cxp 5110  dom cdm 5112  ran crn 5113  Ord word 5720  Oncon0 5721  cio 5847   Fn wfn 5881  wf 5882  ontowfo 5884  cfv 5886   Isom wiso 5887  (class class class)co 6647  cmpt2 6649  1st c1st 7163  2nd c2nd 7164   supp csupp 7292  seq𝜔cseqom 7539   +𝑜 coa 7554   ·𝑜 comu 7555  𝑜 coe 7556  cen 7949   finSupp cfsupp 8272  OrdIsocoi 8411   CNF ccnf 8555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-supp 7293  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-seqom 7540  df-1o 7557  df-2o 7558  df-oadd 7561  df-omul 7562  df-oexp 7563  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-fsupp 8273  df-oi 8412  df-cnf 8556
This theorem is referenced by:  oemapwe  8588  cantnffval2  8589  cantnff1o  8590
  Copyright terms: Public domain W3C validator