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

Theorem cantnf 8534
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 8518, 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 8523 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 7562 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
72, 3, 6syl2anc 692 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ∈ On)
8 eloni 5692 . . . 4 ((𝐴𝑜 𝐵) ∈ On → Ord (𝐴𝑜 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴𝑜 𝐵))
10 ordwe 5695 . . 3 (Ord (𝐴𝑜 𝐵) → E We (𝐴𝑜 𝐵))
11 weso 5065 . . 3 ( E We (𝐴𝑜 𝐵) → E Or (𝐴𝑜 𝐵))
12 sopo 5012 . . 3 ( E Or (𝐴𝑜 𝐵) → E Po (𝐴𝑜 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴𝑜 𝐵))
141, 2, 3cantnff 8515 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
15 frn 6010 . . . . 5 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
1614, 15syl 17 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
17 onss 6937 . . . . . . . 8 ((𝐴𝑜 𝐵) ∈ On → (𝐴𝑜 𝐵) ⊆ On)
187, 17syl 17 . . . . . . 7 (𝜑 → (𝐴𝑜 𝐵) ⊆ On)
1918sseld 3582 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ On))
20 eleq1 2686 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴𝑜 𝐵) ↔ 𝑦 ∈ (𝐴𝑜 𝐵)))
21 eleq1 2686 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2220, 21imbi12d 334 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2322imbi2d 330 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
24 r19.21v 2954 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
25 ordelss 5698 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴𝑜 𝐵) ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
269, 25sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
2726sselda 3583 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴𝑜 𝐵))
28 pm5.5 351 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝑜 𝐵) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2927, 28syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
3029ralbidva 2979 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
31 dfss3 3573 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3230, 31syl6bbr 278 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
33 eleq1 2686 . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴𝑜 𝐵))
39 simplrr 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
407adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ∈ On)
41 simprl 793 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴𝑜 𝐵))
42 onelon 5707 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑜 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ∈ On)
4340, 41, 42syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
44 on0eln0 5739 . . . . . . . . . . . . . . . . . . 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 8533 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
52 fczsupp0 7269 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5352eqcomi 2630 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
54 oieq2 8362 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
56 ne0i 3897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵𝐵 ≠ ∅)
57 ne0i 3897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ (𝐴𝑜 𝐵) → (𝐴𝑜 𝐵) ≠ ∅)
5857ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ≠ ∅)
59 oveq1 6611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
6059neeq1d 2849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ≠ ∅ ↔ (∅ ↑𝑜 𝐵) ≠ ∅))
6158, 60syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑𝑜 𝐵) ≠ ∅))
6261necon2d 2813 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅))
63 on0eln0 5739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
64 oe0m1 7546 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
6563, 64bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
6636, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
67 on0eln0 5739 . . . . . . . . . . . . . . . . . . . . . . . . 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 5123 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7371, 72fmptd 6340 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
74 0ex 4750 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
763, 75fczfsuppd 8237 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7776adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
781, 2, 3cantnfs 8507 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7978adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
8073, 77, 79mpbir2and 956 . . . . . . . . . . . . . . . . . . 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 8509 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)))
83 we0 5069 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
84 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8584oien 8387 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8674, 83, 85mp2an 707 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
87 en0 7963 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8886, 87mpbi 220 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8988fveq2i 6151 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅)
9081seqom0g 7496 . . . . . . . . . . . . . . . . . . . 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 6002 . . . . . . . . . . . . . . . . . . 19 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆)
9694, 95syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
97 fnfvelrn 6312 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9896, 80, 97syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9993, 98eqeltrrd 2699 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
10033, 51, 99pm2.61ne 2875 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
101100expr 642 . . . . . . . . . . . . . 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 7003 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
109108com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
11019, 109mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
111110ssrdv 3589 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵))
11216, 111eqssd 3600 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵))
113 dffo2 6076 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵)))
11414, 112, 113sylanbrc 697 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵))
1152adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1163adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
117 fveq2 6148 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
118 fveq2 6148 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
119117, 118eleq12d 2692 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
120 eleq1 2686 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
121120imbi1d 331 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
122121ralbidv 2980 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
123119, 122anbi12d 746 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
124123cbvrexv 3160 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
125 fveq1 6147 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
126 fveq1 6147 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
127 eleq12 2688 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
128125, 126, 127syl2an 494 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
129 fveq1 6147 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
130 fveq1 6147 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
131129, 130eqeqan12d 2637 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
132131imbi2d 330 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
133132ralbidv 2980 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
134128, 133anbi12d 746 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
135134rexbidv 3045 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
136124, 135syl5bb 272 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
137136cbvopabv 4684 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1384, 137eqtri 2643 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
139 simprll 801 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
140 simprlr 802 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
141 simprr 795 . . . . . 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 8530 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
146 fvex 6158 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
147146epelc 4987 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
148145, 147sylibr 224 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
149148expr 642 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
150149ralrimivva 2965 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
151 soisoi 6532 . 2 (((𝑇 Or 𝑆 ∧ E Po (𝐴𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ∧ ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
1525, 13, 114, 150, 151syl22anc 1324 1 (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  wss 3555  c0 3891  {csn 4148  cop 4154   cuni 4402   cint 4440   class class class wbr 4613  {copab 4672   E cep 4983   Po wpo 4993   Or wor 4994   We wwe 5032   × cxp 5072  dom cdm 5074  ran crn 5075  Ord word 5681  Oncon0 5682  cio 5808   Fn wfn 5842  wf 5843  ontowfo 5845  cfv 5847   Isom wiso 5848  (class class class)co 6604  cmpt2 6606  1st c1st 7111  2nd c2nd 7112   supp csupp 7240  seq𝜔cseqom 7487   +𝑜 coa 7502   ·𝑜 comu 7503  𝑜 coe 7504  cen 7896   finSupp cfsupp 8219  OrdIsocoi 8358   CNF ccnf 8502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-seqom 7488  df-1o 7505  df-2o 7506  df-oadd 7509  df-omul 7510  df-oexp 7511  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-oi 8359  df-cnf 8503
This theorem is referenced by:  oemapwe  8535  cantnffval2  8536  cantnff1o  8537
  Copyright terms: Public domain W3C validator