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  –onto→wfo 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