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

Theorem cantnf 8753
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 8737, 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 8742 . 2 (𝜑𝑇 Or 𝑆)
6 oecl 7770 . . . . 5 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
72, 3, 6syl2anc 565 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ∈ On)
8 eloni 5876 . . . 4 ((𝐴𝑜 𝐵) ∈ On → Ord (𝐴𝑜 𝐵))
97, 8syl 17 . . 3 (𝜑 → Ord (𝐴𝑜 𝐵))
10 ordwe 5879 . . 3 (Ord (𝐴𝑜 𝐵) → E We (𝐴𝑜 𝐵))
11 weso 5240 . . 3 ( E We (𝐴𝑜 𝐵) → E Or (𝐴𝑜 𝐵))
12 sopo 5187 . . 3 ( E Or (𝐴𝑜 𝐵) → E Po (𝐴𝑜 𝐵))
139, 10, 11, 124syl 19 . 2 (𝜑 → E Po (𝐴𝑜 𝐵))
141, 2, 3cantnff 8734 . . 3 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
15 frn 6193 . . . . 5 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
1614, 15syl 17 . . . 4 (𝜑 → ran (𝐴 CNF 𝐵) ⊆ (𝐴𝑜 𝐵))
17 onss 7136 . . . . . . . 8 ((𝐴𝑜 𝐵) ∈ On → (𝐴𝑜 𝐵) ⊆ On)
187, 17syl 17 . . . . . . 7 (𝜑 → (𝐴𝑜 𝐵) ⊆ On)
1918sseld 3749 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ On))
20 eleq1w 2832 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ (𝐴𝑜 𝐵) ↔ 𝑦 ∈ (𝐴𝑜 𝐵)))
21 eleq1w 2832 . . . . . . . . . 10 (𝑡 = 𝑦 → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2220, 21imbi12d 333 . . . . . . . . 9 (𝑡 = 𝑦 → ((𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)) ↔ (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
2322imbi2d 329 . . . . . . . 8 (𝑡 = 𝑦 → ((𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)))))
24 r19.21v 3108 . . . . . . . . 9 (∀𝑦𝑡 (𝜑 → (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))) ↔ (𝜑 → ∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵))))
25 ordelss 5882 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐴𝑜 𝐵) ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
269, 25sylan 561 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ⊆ (𝐴𝑜 𝐵))
2726sselda 3750 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → 𝑦 ∈ (𝐴𝑜 𝐵))
28 pm5.5 350 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝑜 𝐵) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
2927, 28syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) ∧ 𝑦𝑡) → ((𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑦 ∈ ran (𝐴 CNF 𝐵)))
3029ralbidva 3133 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵)))
31 dfss3 3739 . . . . . . . . . . . . . . 15 (𝑡 ⊆ ran (𝐴 CNF 𝐵) ↔ ∀𝑦𝑡 𝑦 ∈ ran (𝐴 CNF 𝐵))
3230, 31syl6bbr 278 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) ↔ 𝑡 ⊆ ran (𝐴 CNF 𝐵)))
33 eleq1 2837 . . . . . . . . . . . . . . . 16 (𝑡 = ∅ → (𝑡 ∈ ran (𝐴 CNF 𝐵) ↔ ∅ ∈ ran (𝐴 CNF 𝐵)))
342adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐴 ∈ On)
3534adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐴 ∈ On)
363adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝐵 ∈ On)
3736adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝐵 ∈ On)
38 simplrl 754 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ (𝐴𝑜 𝐵))
39 simplrr 755 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ⊆ ran (𝐴 CNF 𝐵))
407adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ∈ On)
41 simprl 746 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ (𝐴𝑜 𝐵))
42 onelon 5891 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑜 𝐵) ∈ On ∧ 𝑡 ∈ (𝐴𝑜 𝐵)) → 𝑡 ∈ On)
4340, 41, 42syl2anc 565 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ On)
44 on0eln0 5923 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ On → (∅ ∈ 𝑡𝑡 ≠ ∅))
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝑡𝑡 ≠ ∅))
4645biimpar 463 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → ∅ ∈ 𝑡)
47 eqid 2770 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)} = {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}
48 eqid 2770 . . . . . . . . . . . . . . . . 17 (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)) = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))
49 eqid 2770 . . . . . . . . . . . . . . . . 17 (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (1st ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
50 eqid 2770 . . . . . . . . . . . . . . . . 17 (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡))) = (2nd ‘(℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)})(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 {𝑐 ∈ On ∣ 𝑡 ∈ (𝐴𝑜 𝑐)}) ·𝑜 𝑎) +𝑜 𝑏) = 𝑡)))
511, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50cantnflem4 8752 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑡 ≠ ∅) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
52 fczsupp0 7475 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 × {∅}) supp ∅) = ∅
5352eqcomi 2779 . . . . . . . . . . . . . . . . . . . 20 ∅ = ((𝐵 × {∅}) supp ∅)
54 oieq2 8573 . . . . . . . . . . . . . . . . . . . 20 (∅ = ((𝐵 × {∅}) supp ∅) → OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅)))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , ∅) = OrdIso( E , ((𝐵 × {∅}) supp ∅))
56 ne0i 4067 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵𝐵 ≠ ∅)
57 ne0i 4067 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ (𝐴𝑜 𝐵) → (𝐴𝑜 𝐵) ≠ ∅)
5857ad2antrl 699 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴𝑜 𝐵) ≠ ∅)
59 oveq1 6799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
6059neeq1d 3001 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ≠ ∅ ↔ (∅ ↑𝑜 𝐵) ≠ ∅))
6158, 60syl5ibcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 = ∅ → (∅ ↑𝑜 𝐵) ≠ ∅))
6261necon2d 2965 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((∅ ↑𝑜 𝐵) = ∅ → 𝐴 ≠ ∅))
63 on0eln0 5923 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵𝐵 ≠ ∅))
64 oe0m1 7754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
6563, 64bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵 ∈ On → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
6636, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ ↔ (∅ ↑𝑜 𝐵) = ∅))
67 on0eln0 5923 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
6834, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (∅ ∈ 𝐴𝐴 ≠ ∅))
6962, 66, 683imtr4d 283 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 ≠ ∅ → ∅ ∈ 𝐴))
7056, 69syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝑦𝐵 → ∅ ∈ 𝐴))
7170imp 393 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) ∧ 𝑦𝐵) → ∅ ∈ 𝐴)
72 fconstmpt 5303 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 × {∅}) = (𝑦𝐵 ↦ ∅)
7371, 72fmptd 6527 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}):𝐵𝐴)
74 0ex 4921 . . . . . . . . . . . . . . . . . . . . . . 23 ∅ ∈ V
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∅ ∈ V)
763, 75fczfsuppd 8448 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 × {∅}) finSupp ∅)
7776adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) finSupp ∅)
781, 2, 3cantnfs 8726 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
7978adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
8073, 77, 79mpbir2and 684 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐵 × {∅}) ∈ 𝑆)
81 eqid 2770 . . . . . . . . . . . . . . . . . . 19 seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)
821, 34, 36, 55, 80, 81cantnfval 8728 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)))
83 we0 5244 . . . . . . . . . . . . . . . . . . . . . 22 E We ∅
84 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , ∅) = OrdIso( E , ∅)
8584oien 8598 . . . . . . . . . . . . . . . . . . . . . 22 ((∅ ∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈ ∅)
8674, 83, 85mp2an 664 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , ∅) ≈ ∅
87 en0 8171 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) = ∅)
8886, 87mpbi 220 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , ∅) = ∅
8988fveq2i 6335 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅)
9081seqom0g 7703 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ V → (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅)
9174, 90ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘∅) = ∅
9289, 91eqtri 2792 . . . . . . . . . . . . . . . . . 18 (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , ∅)‘𝑘)) ·𝑜 ((𝐵 × {∅})‘(OrdIso( E , ∅)‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ∅)) = ∅
9382, 92syl6eq 2820 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
9414adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
95 ffn 6185 . . . . . . . . . . . . . . . . . . 19 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆)
9694, 95syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → (𝐴 CNF 𝐵) Fn 𝑆)
97 fnfvelrn 6499 . . . . . . . . . . . . . . . . . 18 (((𝐴 CNF 𝐵) Fn 𝑆 ∧ (𝐵 × {∅}) ∈ 𝑆) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9896, 80, 97syl2anc 565 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) ∈ ran (𝐴 CNF 𝐵))
9993, 98eqeltrrd 2850 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → ∅ ∈ ran (𝐴 CNF 𝐵))
10033, 51, 99pm2.61ne 3027 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑡 ∈ (𝐴𝑜 𝐵) ∧ 𝑡 ⊆ ran (𝐴 CNF 𝐵))) → 𝑡 ∈ ran (𝐴 CNF 𝐵))
101100expr 444 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (𝑡 ⊆ ran (𝐴 CNF 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
10232, 101sylbid 230 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ (𝐴𝑜 𝐵)) → (∀𝑦𝑡 (𝑦 ∈ (𝐴𝑜 𝐵) → 𝑦 ∈ ran (𝐴 CNF 𝐵)) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
103102ex 397 . . . . . . . . . . . 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 7202 . . . . . . 7 (𝑡 ∈ On → (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
109108com3l 89 . . . . . 6 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → (𝑡 ∈ On → 𝑡 ∈ ran (𝐴 CNF 𝐵))))
11019, 109mpdd 43 . . . . 5 (𝜑 → (𝑡 ∈ (𝐴𝑜 𝐵) → 𝑡 ∈ ran (𝐴 CNF 𝐵)))
111110ssrdv 3756 . . . 4 (𝜑 → (𝐴𝑜 𝐵) ⊆ ran (𝐴 CNF 𝐵))
11216, 111eqssd 3767 . . 3 (𝜑 → ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵))
113 dffo2 6260 . . 3 ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ↔ ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) ∧ ran (𝐴 CNF 𝐵) = (𝐴𝑜 𝐵)))
11414, 112, 113sylanbrc 564 . 2 (𝜑 → (𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵))
1152adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐴 ∈ On)
1163adantr 466 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝐵 ∈ On)
117 fveq2 6332 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑥𝑧) = (𝑥𝑡))
118 fveq2 6332 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝑦𝑧) = (𝑦𝑡))
119117, 118eleq12d 2843 . . . . . . . . . . 11 (𝑧 = 𝑡 → ((𝑥𝑧) ∈ (𝑦𝑧) ↔ (𝑥𝑡) ∈ (𝑦𝑡)))
120 eleq1w 2832 . . . . . . . . . . . . 13 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
121120imbi1d 330 . . . . . . . . . . . 12 (𝑧 = 𝑡 → ((𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
122121ralbidv 3134 . . . . . . . . . . 11 (𝑧 = 𝑡 → (∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
123119, 122anbi12d 608 . . . . . . . . . 10 (𝑧 = 𝑡 → (((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)))))
124123cbvrexv 3320 . . . . . . . . 9 (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))))
125 fveq1 6331 . . . . . . . . . . . 12 (𝑥 = 𝑢 → (𝑥𝑡) = (𝑢𝑡))
126 fveq1 6331 . . . . . . . . . . . 12 (𝑦 = 𝑣 → (𝑦𝑡) = (𝑣𝑡))
127 eleq12 2839 . . . . . . . . . . . 12 (((𝑥𝑡) = (𝑢𝑡) ∧ (𝑦𝑡) = (𝑣𝑡)) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
128125, 126, 127syl2an 575 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑡) ∈ (𝑦𝑡) ↔ (𝑢𝑡) ∈ (𝑣𝑡)))
129 fveq1 6331 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (𝑥𝑤) = (𝑢𝑤))
130 fveq1 6331 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → (𝑦𝑤) = (𝑣𝑤))
131129, 130eqeqan12d 2786 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑤) = (𝑦𝑤) ↔ (𝑢𝑤) = (𝑣𝑤)))
132131imbi2d 329 . . . . . . . . . . . 12 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
133132ralbidv 3134 . . . . . . . . . . 11 ((𝑥 = 𝑢𝑦 = 𝑣) → (∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤))))
134128, 133anbi12d 608 . . . . . . . . . 10 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
135134rexbidv 3199 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑡𝐵 ((𝑥𝑡) ∈ (𝑦𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
136124, 135syl5bb 272 . . . . . . . 8 ((𝑥 = 𝑢𝑦 = 𝑣) → (∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))))
137136cbvopabv 4854 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
1384, 137eqtri 2792 . . . . . 6 𝑇 = {⟨𝑢, 𝑣⟩ ∣ ∃𝑡𝐵 ((𝑢𝑡) ∈ (𝑣𝑡) ∧ ∀𝑤𝐵 (𝑡𝑤 → (𝑢𝑤) = (𝑣𝑤)))}
139 simprll 756 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑆)
140 simprlr 757 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑔𝑆)
141 simprr 748 . . . . . 6 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → 𝑓𝑇𝑔)
142 eqid 2770 . . . . . 6 {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)} = {𝑐𝐵 ∣ (𝑓𝑐) ∈ (𝑔𝑐)}
143 eqid 2770 . . . . . 6 OrdIso( E , (𝑔 supp ∅)) = OrdIso( E , (𝑔 supp ∅))
144 eqid 2770 . . . . . 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 8749 . . . . 5 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
146 fvex 6342 . . . . . 6 ((𝐴 CNF 𝐵)‘𝑔) ∈ V
147146epelc 5164 . . . . 5 (((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔) ↔ ((𝐴 CNF 𝐵)‘𝑓) ∈ ((𝐴 CNF 𝐵)‘𝑔))
148145, 147sylibr 224 . . . 4 ((𝜑 ∧ ((𝑓𝑆𝑔𝑆) ∧ 𝑓𝑇𝑔)) → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔))
149148expr 444 . . 3 ((𝜑 ∧ (𝑓𝑆𝑔𝑆)) → (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
150149ralrimivva 3119 . 2 (𝜑 → ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))
151 soisoi 6720 . 2 (((𝑇 Or 𝑆 ∧ E Po (𝐴𝑜 𝐵)) ∧ ((𝐴 CNF 𝐵):𝑆onto→(𝐴𝑜 𝐵) ∧ ∀𝑓𝑆𝑔𝑆 (𝑓𝑇𝑔 → ((𝐴 CNF 𝐵)‘𝑓) E ((𝐴 CNF 𝐵)‘𝑔)))) → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
1525, 13, 114, 150, 151syl22anc 1476 1 (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴𝑜 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wcel 2144  wne 2942  wral 3060  wrex 3061  {crab 3064  Vcvv 3349  wss 3721  c0 4061  {csn 4314  cop 4320   cuni 4572   cint 4609   class class class wbr 4784  {copab 4844   E cep 5161   Po wpo 5168   Or wor 5169   We wwe 5207   × cxp 5247  dom cdm 5249  ran crn 5250  Ord word 5865  Oncon0 5866  cio 5992   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031   Isom wiso 6032  (class class class)co 6792  cmpt2 6794  1st c1st 7312  2nd c2nd 7313   supp csupp 7445  seq𝜔cseqom 7694   +𝑜 coa 7709   ·𝑜 comu 7710  𝑜 coe 7711  cen 8105   finSupp cfsupp 8430  OrdIsocoi 8569   CNF ccnf 8721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-supp 7446  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-seqom 7695  df-1o 7712  df-2o 7713  df-oadd 7716  df-omul 7717  df-oexp 7718  df-er 7895  df-map 8010  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fsupp 8431  df-oi 8570  df-cnf 8722
This theorem is referenced by:  oemapwe  8754  cantnffval2  8755  cantnff1o  8756
  Copyright terms: Public domain W3C validator