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

Theorem cantnflem3 9732
Description: Lemma for cantnf 9734. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than 𝐶 has a normal form, we can use oeeu 8642 to factor 𝐶 into the form ((𝐴o 𝑋) ·o 𝑌) +o 𝑍 where 0 < 𝑌 < 𝐴 and 𝑍 < (𝐴o 𝑋) (and a fortiori 𝑋 < 𝐵). Then since 𝑍 < (𝐴o 𝑋) ≤ (𝐴o 𝑋) ·o 𝑌𝐶, 𝑍 has a normal form, and by appending the term (𝐴o 𝑋) ·o 𝑌 using cantnfp1 9722 we get a normal form for 𝐶. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
oemapval.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
cantnf.c (𝜑𝐶 ∈ (𝐴o 𝐵))
cantnf.s (𝜑𝐶 ⊆ ran (𝐴 CNF 𝐵))
cantnf.e (𝜑 → ∅ ∈ 𝐶)
cantnf.x 𝑋 = {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴o 𝑐)}
cantnf.p 𝑃 = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o 𝑋) ·o 𝑎) +o 𝑏) = 𝐶))
cantnf.y 𝑌 = (1st𝑃)
cantnf.z 𝑍 = (2nd𝑃)
cantnf.g (𝜑𝐺𝑆)
cantnf.v (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
cantnf.f 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
Assertion
Ref Expression
cantnflem3 (𝜑𝐶 ∈ ran (𝐴 CNF 𝐵))
Distinct variable groups:   𝑡,𝑐,𝑤,𝑥,𝑦,𝑧,𝐵   𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧,𝐶   𝑡,𝑎,𝐴,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝑇,𝑐,𝑡   𝑤,𝐹,𝑥,𝑦,𝑧   𝑆,𝑐,𝑡,𝑥,𝑦,𝑧   𝑡,𝑍,𝑥,𝑦,𝑧   𝐺,𝑐,𝑡,𝑤,𝑥,𝑦,𝑧   𝜑,𝑡,𝑥,𝑦,𝑧   𝑡,𝑌,𝑤,𝑥,𝑦,𝑧   𝑋,𝑎,𝑏,𝑑,𝑡,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑤,𝑎,𝑏,𝑐,𝑑)   𝐵(𝑎,𝑏,𝑑)   𝐶(𝑡)   𝑃(𝑥,𝑦,𝑧,𝑤,𝑡,𝑎,𝑏,𝑐,𝑑)   𝑆(𝑤,𝑎,𝑏,𝑑)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑎,𝑏,𝑑)   𝐹(𝑡,𝑎,𝑏,𝑐,𝑑)   𝐺(𝑎,𝑏,𝑑)   𝑋(𝑐)   𝑌(𝑎,𝑏,𝑐,𝑑)   𝑍(𝑤,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem cantnflem3
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . . . 5 𝑆 = dom (𝐴 CNF 𝐵)
2 cantnfs.a . . . . 5 (𝜑𝐴 ∈ On)
3 cantnfs.b . . . . 5 (𝜑𝐵 ∈ On)
4 cantnf.g . . . . 5 (𝜑𝐺𝑆)
5 oemapval.t . . . . . . . . . . . . . 14 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
6 cantnf.c . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ (𝐴o 𝐵))
7 cantnf.s . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ran (𝐴 CNF 𝐵))
8 cantnf.e . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ 𝐶)
91, 2, 3, 5, 6, 7, 8cantnflem2 9731 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
10 eqid 2736 . . . . . . . . . . . . . . 15 𝑋 = 𝑋
11 eqid 2736 . . . . . . . . . . . . . . 15 𝑌 = 𝑌
12 eqid 2736 . . . . . . . . . . . . . . 15 𝑍 = 𝑍
1310, 11, 123pm3.2i 1339 . . . . . . . . . . . . . 14 (𝑋 = 𝑋𝑌 = 𝑌𝑍 = 𝑍)
14 cantnf.x . . . . . . . . . . . . . . 15 𝑋 = {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴o 𝑐)}
15 cantnf.p . . . . . . . . . . . . . . 15 𝑃 = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴o 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴o 𝑋) ·o 𝑎) +o 𝑏) = 𝐶))
16 cantnf.y . . . . . . . . . . . . . . 15 𝑌 = (1st𝑃)
17 cantnf.z . . . . . . . . . . . . . . 15 𝑍 = (2nd𝑃)
1814, 15, 16, 17oeeui 8641 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)) → (((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶) ↔ (𝑋 = 𝑋𝑌 = 𝑌𝑍 = 𝑍)))
1913, 18mpbiri 258 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)) → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶))
209, 19syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶))
2120simpld 494 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)))
2221simp1d 1142 . . . . . . . . . 10 (𝜑𝑋 ∈ On)
23 oecl 8576 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
242, 22, 23syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐴o 𝑋) ∈ On)
2521simp2d 1143 . . . . . . . . . . 11 (𝜑𝑌 ∈ (𝐴 ∖ 1o))
2625eldifad 3962 . . . . . . . . . 10 (𝜑𝑌𝐴)
27 onelon 6408 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
282, 26, 27syl2anc 584 . . . . . . . . 9 (𝜑𝑌 ∈ On)
29 dif1o 8539 . . . . . . . . . . . 12 (𝑌 ∈ (𝐴 ∖ 1o) ↔ (𝑌𝐴𝑌 ≠ ∅))
3029simprbi 496 . . . . . . . . . . 11 (𝑌 ∈ (𝐴 ∖ 1o) → 𝑌 ≠ ∅)
3125, 30syl 17 . . . . . . . . . 10 (𝜑𝑌 ≠ ∅)
32 on0eln0 6439 . . . . . . . . . . 11 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
3328, 32syl 17 . . . . . . . . . 10 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
3431, 33mpbird 257 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝑌)
35 omword1 8612 . . . . . . . . 9 ((((𝐴o 𝑋) ∈ On ∧ 𝑌 ∈ On) ∧ ∅ ∈ 𝑌) → (𝐴o 𝑋) ⊆ ((𝐴o 𝑋) ·o 𝑌))
3624, 28, 34, 35syl21anc 837 . . . . . . . 8 (𝜑 → (𝐴o 𝑋) ⊆ ((𝐴o 𝑋) ·o 𝑌))
37 omcl 8575 . . . . . . . . . . 11 (((𝐴o 𝑋) ∈ On ∧ 𝑌 ∈ On) → ((𝐴o 𝑋) ·o 𝑌) ∈ On)
3824, 28, 37syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ∈ On)
3921simp3d 1144 . . . . . . . . . . 11 (𝜑𝑍 ∈ (𝐴o 𝑋))
40 onelon 6408 . . . . . . . . . . 11 (((𝐴o 𝑋) ∈ On ∧ 𝑍 ∈ (𝐴o 𝑋)) → 𝑍 ∈ On)
4124, 39, 40syl2anc 584 . . . . . . . . . 10 (𝜑𝑍 ∈ On)
42 oaword1 8591 . . . . . . . . . 10 ((((𝐴o 𝑋) ·o 𝑌) ∈ On ∧ 𝑍 ∈ On) → ((𝐴o 𝑋) ·o 𝑌) ⊆ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
4338, 41, 42syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ⊆ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
4420simprd 495 . . . . . . . . 9 (𝜑 → (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶)
4543, 44sseqtrd 4019 . . . . . . . 8 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ⊆ 𝐶)
4636, 45sstrd 3993 . . . . . . 7 (𝜑 → (𝐴o 𝑋) ⊆ 𝐶)
47 oecl 8576 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
482, 3, 47syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴o 𝐵) ∈ On)
49 ontr2 6430 . . . . . . . 8 (((𝐴o 𝑋) ∈ On ∧ (𝐴o 𝐵) ∈ On) → (((𝐴o 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴o 𝐵)) → (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5024, 48, 49syl2anc 584 . . . . . . 7 (𝜑 → (((𝐴o 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴o 𝐵)) → (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5146, 6, 50mp2and 699 . . . . . 6 (𝜑 → (𝐴o 𝑋) ∈ (𝐴o 𝐵))
529simpld 494 . . . . . . 7 (𝜑𝐴 ∈ (On ∖ 2o))
53 oeord 8627 . . . . . . 7 ((𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑋𝐵 ↔ (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5422, 3, 52, 53syl3anc 1372 . . . . . 6 (𝜑 → (𝑋𝐵 ↔ (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5551, 54mpbird 257 . . . . 5 (𝜑𝑋𝐵)
562adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ On)
573adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐵 ∈ On)
58 suppssdm 8203 . . . . . . . . . . . . . . 15 (𝐺 supp ∅) ⊆ dom 𝐺
591, 2, 3cantnfs 9707 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
604, 59mpbid 232 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
6160simpld 494 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝐵𝐴)
6258, 61fssdm 6754 . . . . . . . . . . . . . 14 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
6362sselda 3982 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝐵)
64 onelon 6408 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
6557, 63, 64syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ On)
66 oecl 8576 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴o 𝑥) ∈ On)
6756, 65, 66syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ∈ On)
6861adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺:𝐵𝐴)
6968, 63ffvelcdmd 7104 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ 𝐴)
70 onelon 6408 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺𝑥) ∈ 𝐴) → (𝐺𝑥) ∈ On)
7156, 69, 70syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ On)
7261ffnd 6736 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐵)
738elexd 3503 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
74 elsuppfn 8196 . . . . . . . . . . . . . 14 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
7572, 3, 73, 74syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
7675simplbda 499 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ≠ ∅)
77 on0eln0 6439 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ On → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
7871, 77syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
7976, 78mpbird 257 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ∅ ∈ (𝐺𝑥))
80 omword1 8612 . . . . . . . . . . 11 ((((𝐴o 𝑥) ∈ On ∧ (𝐺𝑥) ∈ On) ∧ ∅ ∈ (𝐺𝑥)) → (𝐴o 𝑥) ⊆ ((𝐴o 𝑥) ·o (𝐺𝑥)))
8167, 71, 79, 80syl21anc 837 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ⊆ ((𝐴o 𝑥) ·o (𝐺𝑥)))
82 eqid 2736 . . . . . . . . . . . 12 OrdIso( E , (𝐺 supp ∅)) = OrdIso( E , (𝐺 supp ∅))
834adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺𝑆)
84 eqid 2736 . . . . . . . . . . . 12 seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·o (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·o (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +o 𝑧)), ∅)
851, 56, 57, 82, 83, 84, 63cantnfle 9712 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴o 𝑥) ·o (𝐺𝑥)) ⊆ ((𝐴 CNF 𝐵)‘𝐺))
86 cantnf.v . . . . . . . . . . . 12 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
8786adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
8885, 87sseqtrd 4019 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴o 𝑥) ·o (𝐺𝑥)) ⊆ 𝑍)
8981, 88sstrd 3993 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ⊆ 𝑍)
9039adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑍 ∈ (𝐴o 𝑋))
9124adantr 480 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑋) ∈ On)
92 ontr2 6430 . . . . . . . . . 10 (((𝐴o 𝑥) ∈ On ∧ (𝐴o 𝑋) ∈ On) → (((𝐴o 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴o 𝑋)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9367, 91, 92syl2anc 584 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (((𝐴o 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴o 𝑋)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9489, 90, 93mp2and 699 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋))
9522adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑋 ∈ On)
9652adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ (On ∖ 2o))
97 oeord 8627 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑥𝑋 ↔ (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9865, 95, 96, 97syl3anc 1372 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝑥𝑋 ↔ (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9994, 98mpbird 257 . . . . . . 7 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝑋)
10099ex 412 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) → 𝑥𝑋))
101100ssrdv 3988 . . . . 5 (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
102 cantnf.f . . . . 5 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
1031, 2, 3, 4, 55, 26, 101, 102cantnfp1 9722 . . . 4 (𝜑 → (𝐹𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))))
104103simprd 495 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
10586oveq2d 7448 . . 3 (𝜑 → (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)) = (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
106104, 105, 443eqtrd 2780 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = 𝐶)
1071, 2, 3cantnff 9715 . . . 4 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
108107ffnd 6736 . . 3 (𝜑 → (𝐴 CNF 𝐵) Fn 𝑆)
109103simpld 494 . . 3 (𝜑𝐹𝑆)
110 fnfvelrn 7099 . . 3 (((𝐴 CNF 𝐵) Fn 𝑆𝐹𝑆) → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
111108, 109, 110syl2anc 584 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
112106, 111eqeltrrd 2841 1 (𝜑𝐶 ∈ ran (𝐴 CNF 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  Vcvv 3479  cdif 3947  wss 3950  c0 4332  ifcif 4524  cop 4631   cuni 4906   cint 4945   class class class wbr 5142  {copab 5204  cmpt 5224   E cep 5582  dom cdm 5684  ran crn 5685  Oncon0 6383  cio 6511   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  cmpo 7434  1st c1st 8013  2nd c2nd 8014   supp csupp 8186  seqωcseqom 8488  1oc1o 8500  2oc2o 8501   +o coa 8504   ·o comu 8505  o coe 8506   finSupp cfsupp 9402  OrdIsocoi 9550   CNF ccnf 9702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-seqom 8489  df-1o 8507  df-2o 8508  df-oadd 8511  df-omul 8512  df-oexp 8513  df-er 8746  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-oi 9551  df-cnf 9703
This theorem is referenced by:  cantnflem4  9733
  Copyright terms: Public domain W3C validator