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

Theorem cantnflem3 9142
 Description: Lemma for cantnf 9144. 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 8216 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 9132 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 9141 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)))
10 eqid 2801 . . . . . . . . . . . . . . 15 𝑋 = 𝑋
11 eqid 2801 . . . . . . . . . . . . . . 15 𝑌 = 𝑌
12 eqid 2801 . . . . . . . . . . . . . . 15 𝑍 = 𝑍
1310, 11, 123pm3.2i 1336 . . . . . . . . . . . . . 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 8215 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)) → (((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶) ↔ (𝑋 = 𝑋𝑌 = 𝑌𝑍 = 𝑍)))
1913, 18mpbiri 261 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2o) ∧ 𝐶 ∈ (On ∖ 1o)) → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶))
209, 19syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)) ∧ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶))
2120simpld 498 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴o 𝑋)))
2221simp1d 1139 . . . . . . . . . 10 (𝜑𝑋 ∈ On)
23 oecl 8149 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴o 𝑋) ∈ On)
242, 22, 23syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐴o 𝑋) ∈ On)
2521simp2d 1140 . . . . . . . . . . 11 (𝜑𝑌 ∈ (𝐴 ∖ 1o))
2625eldifad 3896 . . . . . . . . . 10 (𝜑𝑌𝐴)
27 onelon 6188 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
282, 26, 27syl2anc 587 . . . . . . . . 9 (𝜑𝑌 ∈ On)
29 dif1o 8112 . . . . . . . . . . . 12 (𝑌 ∈ (𝐴 ∖ 1o) ↔ (𝑌𝐴𝑌 ≠ ∅))
3029simprbi 500 . . . . . . . . . . 11 (𝑌 ∈ (𝐴 ∖ 1o) → 𝑌 ≠ ∅)
3125, 30syl 17 . . . . . . . . . 10 (𝜑𝑌 ≠ ∅)
32 on0eln0 6218 . . . . . . . . . . 11 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
3328, 32syl 17 . . . . . . . . . 10 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
3431, 33mpbird 260 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝑌)
35 omword1 8186 . . . . . . . . 9 ((((𝐴o 𝑋) ∈ On ∧ 𝑌 ∈ On) ∧ ∅ ∈ 𝑌) → (𝐴o 𝑋) ⊆ ((𝐴o 𝑋) ·o 𝑌))
3624, 28, 34, 35syl21anc 836 . . . . . . . 8 (𝜑 → (𝐴o 𝑋) ⊆ ((𝐴o 𝑋) ·o 𝑌))
37 omcl 8148 . . . . . . . . . . 11 (((𝐴o 𝑋) ∈ On ∧ 𝑌 ∈ On) → ((𝐴o 𝑋) ·o 𝑌) ∈ On)
3824, 28, 37syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ∈ On)
3921simp3d 1141 . . . . . . . . . . 11 (𝜑𝑍 ∈ (𝐴o 𝑋))
40 onelon 6188 . . . . . . . . . . 11 (((𝐴o 𝑋) ∈ On ∧ 𝑍 ∈ (𝐴o 𝑋)) → 𝑍 ∈ On)
4124, 39, 40syl2anc 587 . . . . . . . . . 10 (𝜑𝑍 ∈ On)
42 oaword1 8165 . . . . . . . . . 10 ((((𝐴o 𝑋) ·o 𝑌) ∈ On ∧ 𝑍 ∈ On) → ((𝐴o 𝑋) ·o 𝑌) ⊆ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
4338, 41, 42syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ⊆ (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
4420simprd 499 . . . . . . . . 9 (𝜑 → (((𝐴o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶)
4543, 44sseqtrd 3958 . . . . . . . 8 (𝜑 → ((𝐴o 𝑋) ·o 𝑌) ⊆ 𝐶)
4636, 45sstrd 3928 . . . . . . 7 (𝜑 → (𝐴o 𝑋) ⊆ 𝐶)
47 oecl 8149 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
482, 3, 47syl2anc 587 . . . . . . . 8 (𝜑 → (𝐴o 𝐵) ∈ On)
49 ontr2 6210 . . . . . . . 8 (((𝐴o 𝑋) ∈ On ∧ (𝐴o 𝐵) ∈ On) → (((𝐴o 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴o 𝐵)) → (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5024, 48, 49syl2anc 587 . . . . . . 7 (𝜑 → (((𝐴o 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴o 𝐵)) → (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5146, 6, 50mp2and 698 . . . . . 6 (𝜑 → (𝐴o 𝑋) ∈ (𝐴o 𝐵))
529simpld 498 . . . . . . 7 (𝜑𝐴 ∈ (On ∖ 2o))
53 oeord 8201 . . . . . . 7 ((𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑋𝐵 ↔ (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5422, 3, 52, 53syl3anc 1368 . . . . . 6 (𝜑 → (𝑋𝐵 ↔ (𝐴o 𝑋) ∈ (𝐴o 𝐵)))
5551, 54mpbird 260 . . . . 5 (𝜑𝑋𝐵)
562adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ On)
573adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐵 ∈ On)
58 suppssdm 7830 . . . . . . . . . . . . . . 15 (𝐺 supp ∅) ⊆ dom 𝐺
591, 2, 3cantnfs 9117 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
604, 59mpbid 235 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
6160simpld 498 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝐵𝐴)
6258, 61fssdm 6508 . . . . . . . . . . . . . 14 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
6362sselda 3918 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝐵)
64 onelon 6188 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
6557, 63, 64syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ On)
66 oecl 8149 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴o 𝑥) ∈ On)
6756, 65, 66syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ∈ On)
6861adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺:𝐵𝐴)
6968, 63ffvelrnd 6833 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ 𝐴)
70 onelon 6188 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺𝑥) ∈ 𝐴) → (𝐺𝑥) ∈ On)
7156, 69, 70syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ On)
7261ffnd 6492 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐵)
738elexd 3464 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
74 elsuppfn 7825 . . . . . . . . . . . . . 14 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
7572, 3, 73, 74syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
7675simplbda 503 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ≠ ∅)
77 on0eln0 6218 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ On → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
7871, 77syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
7976, 78mpbird 260 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ∅ ∈ (𝐺𝑥))
80 omword1 8186 . . . . . . . . . . 11 ((((𝐴o 𝑥) ∈ On ∧ (𝐺𝑥) ∈ On) ∧ ∅ ∈ (𝐺𝑥)) → (𝐴o 𝑥) ⊆ ((𝐴o 𝑥) ·o (𝐺𝑥)))
8167, 71, 79, 80syl21anc 836 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ⊆ ((𝐴o 𝑥) ·o (𝐺𝑥)))
82 eqid 2801 . . . . . . . . . . . 12 OrdIso( E , (𝐺 supp ∅)) = OrdIso( E , (𝐺 supp ∅))
834adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺𝑆)
84 eqid 2801 . . . . . . . . . . . 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 9122 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴o 𝑥) ·o (𝐺𝑥)) ⊆ ((𝐴 CNF 𝐵)‘𝐺))
86 cantnf.v . . . . . . . . . . . 12 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
8786adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
8885, 87sseqtrd 3958 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴o 𝑥) ·o (𝐺𝑥)) ⊆ 𝑍)
8981, 88sstrd 3928 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ⊆ 𝑍)
9039adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑍 ∈ (𝐴o 𝑋))
9124adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑋) ∈ On)
92 ontr2 6210 . . . . . . . . . 10 (((𝐴o 𝑥) ∈ On ∧ (𝐴o 𝑋) ∈ On) → (((𝐴o 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴o 𝑋)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9367, 91, 92syl2anc 587 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (((𝐴o 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴o 𝑋)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9489, 90, 93mp2and 698 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴o 𝑥) ∈ (𝐴o 𝑋))
9522adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑋 ∈ On)
9652adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ (On ∖ 2o))
97 oeord 8201 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2o)) → (𝑥𝑋 ↔ (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9865, 95, 96, 97syl3anc 1368 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝑥𝑋 ↔ (𝐴o 𝑥) ∈ (𝐴o 𝑋)))
9994, 98mpbird 260 . . . . . . 7 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝑋)
10099ex 416 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) → 𝑥𝑋))
101100ssrdv 3924 . . . . 5 (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
102 cantnf.f . . . . 5 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
1031, 2, 3, 4, 55, 26, 101, 102cantnfp1 9132 . . . 4 (𝜑 → (𝐹𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))))
104103simprd 499 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
10586oveq2d 7155 . . 3 (𝜑 → (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)) = (((𝐴o 𝑋) ·o 𝑌) +o 𝑍))
106104, 105, 443eqtrd 2840 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = 𝐶)
1071, 2, 3cantnff 9125 . . . 4 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
108107ffnd 6492 . . 3 (𝜑 → (𝐴 CNF 𝐵) Fn 𝑆)
109103simpld 498 . . 3 (𝜑𝐹𝑆)
110 fnfvelrn 6829 . . 3 (((𝐴 CNF 𝐵) Fn 𝑆𝐹𝑆) → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
111108, 109, 110syl2anc 587 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
112106, 111eqeltrrd 2894 1 (𝜑𝐶 ∈ ran (𝐴 CNF 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  {crab 3113  Vcvv 3444   ∖ cdif 3881   ⊆ wss 3884  ∅c0 4246  ifcif 4428  ⟨cop 4534  ∪ cuni 4803  ∩ cint 4841   class class class wbr 5033  {copab 5095   ↦ cmpt 5113   E cep 5432  dom cdm 5523  ran crn 5524  Oncon0 6163  ℩cio 6285   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141  1st c1st 7673  2nd c2nd 7674   supp csupp 7817  seqωcseqom 8070  1oc1o 8082  2oc2o 8083   +o coa 8086   ·o comu 8087   ↑o coe 8088   finSupp cfsupp 8821  OrdIsocoi 8961   CNF ccnf 9112 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-seqom 8071  df-1o 8089  df-2o 8090  df-oadd 8093  df-omul 8094  df-oexp 8095  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-oi 8962  df-cnf 9113 This theorem is referenced by:  cantnflem4  9143
 Copyright terms: Public domain W3C validator