Step | Hyp | Ref
| Expression |
1 | | cantnfp1.f |
. . . . . 6
⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) |
2 | | cantnfs.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ On) |
3 | | cantnfp1.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
4 | | onelon 5748 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) |
5 | 2, 3, 4 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ On) |
6 | | eloni 5733 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ On → Ord 𝑋) |
7 | | ordirr 5741 |
. . . . . . . . . . . 12
⊢ (Ord
𝑋 → ¬ 𝑋 ∈ 𝑋) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑋) |
9 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘𝑋) ∈ V |
10 | | dif1o 7580 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
↔ ((𝐺‘𝑋) ∈ V ∧ (𝐺‘𝑋) ≠ ∅)) |
11 | 9, 10 | mpbiran 953 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
↔ (𝐺‘𝑋) ≠ ∅) |
12 | | cantnfp1.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
13 | | cantnfs.s |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
14 | | cantnfs.a |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 ∈ On) |
15 | 13, 14, 2 | cantnfs 8563 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
16 | 12, 15 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
17 | 16 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
18 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:𝐵⟶𝐴 → 𝐺 Fn 𝐵) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 Fn 𝐵) |
20 | | 0ex 4790 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∅ ∈
V) |
22 | | elsuppfn 7303 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) |
23 | 19, 2, 21, 22 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) |
24 | 11 | bicomi 214 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑋) ≠ ∅ ↔ (𝐺‘𝑋) ∈ (V ∖
1𝑜)) |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ ↔ (𝐺‘𝑋) ∈ (V ∖
1𝑜))) |
26 | 25 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1𝑜)))) |
27 | 23, 26 | bitrd 268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1𝑜)))) |
28 | | cantnfp1.s |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) |
29 | 28 | sseld 3602 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋 ∈ 𝑋)) |
30 | 27, 29 | sylbird 250 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖ 1𝑜))
→ 𝑋 ∈ 𝑋)) |
31 | 3, 30 | mpand 711 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
→ 𝑋 ∈ 𝑋)) |
32 | 11, 31 | syl5bir 233 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ → 𝑋 ∈ 𝑋)) |
33 | 32 | necon1bd 2812 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝑋 ∈ 𝑋 → (𝐺‘𝑋) = ∅)) |
34 | 8, 33 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) = ∅) |
35 | 34 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ 𝑡 = 𝑋) → (𝐺‘𝑋) = ∅) |
36 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ 𝑡 = 𝑋) → 𝑡 = 𝑋) |
37 | 36 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ 𝑡 = 𝑋) → (𝐺‘𝑡) = (𝐺‘𝑋)) |
38 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ 𝑡 = 𝑋) → 𝑌 = ∅) |
39 | 35, 37, 38 | 3eqtr4rd 2667 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ 𝑡 = 𝑋) → 𝑌 = (𝐺‘𝑡)) |
40 | | eqidd 2623 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) ∧ ¬ 𝑡 = 𝑋) → (𝐺‘𝑡) = (𝐺‘𝑡)) |
41 | 39, 40 | ifeqda 4121 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑌 = ∅) ∧ 𝑡 ∈ 𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = (𝐺‘𝑡)) |
42 | 41 | mpteq2dva 4744 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = ∅) → (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) = (𝑡 ∈ 𝐵 ↦ (𝐺‘𝑡))) |
43 | 1, 42 | syl5eq 2668 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ∅) → 𝐹 = (𝑡 ∈ 𝐵 ↦ (𝐺‘𝑡))) |
44 | 17 | feqmptd 6249 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑡 ∈ 𝐵 ↦ (𝐺‘𝑡))) |
45 | 44 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ∅) → 𝐺 = (𝑡 ∈ 𝐵 ↦ (𝐺‘𝑡))) |
46 | 43, 45 | eqtr4d 2659 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ∅) → 𝐹 = 𝐺) |
47 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ∅) → 𝐺 ∈ 𝑆) |
48 | 46, 47 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = ∅) → 𝐹 ∈ 𝑆) |
49 | | oecl 7617 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
50 | 14, 2, 49 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ∈ On) |
51 | 13, 14, 2 | cantnff 8571 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
52 | 51, 12 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) ∈ (𝐴 ↑𝑜 𝐵)) |
53 | | onelon 5748 |
. . . . . . 7
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘𝐺) ∈ (𝐴 ↑𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘𝐺) ∈ On) |
54 | 50, 52, 53 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) ∈ On) |
55 | 54 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ∅) → ((𝐴 CNF 𝐵)‘𝐺) ∈ On) |
56 | | oa0r 7618 |
. . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝐺) ∈ On → (∅
+𝑜 ((𝐴
CNF 𝐵)‘𝐺)) = ((𝐴 CNF 𝐵)‘𝐺)) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ∅) → (∅
+𝑜 ((𝐴
CNF 𝐵)‘𝐺)) = ((𝐴 CNF 𝐵)‘𝐺)) |
58 | | oveq2 6658 |
. . . . . 6
⊢ (𝑌 = ∅ → ((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌) = ((𝐴 ↑𝑜 𝑋) ·𝑜
∅)) |
59 | | oecl 7617 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑𝑜
𝑋) ∈
On) |
60 | 14, 5, 59 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ∈ On) |
61 | | om0 7597 |
. . . . . . 7
⊢ ((𝐴 ↑𝑜
𝑋) ∈ On → ((𝐴 ↑𝑜
𝑋)
·𝑜 ∅) = ∅) |
62 | 60, 61 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
∅) = ∅) |
63 | 58, 62 | sylan9eqr 2678 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ∅) → ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) =
∅) |
64 | 63 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ∅) → (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)) = (∅ +𝑜 ((𝐴 CNF 𝐵)‘𝐺))) |
65 | 46 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ∅) → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘𝐺)) |
66 | 57, 64, 65 | 3eqtr4rd 2667 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |
67 | 48, 66 | jca 554 |
. 2
⊢ ((𝜑 ∧ 𝑌 = ∅) → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)))) |
68 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝐴 ∈ On) |
69 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝐵 ∈ On) |
70 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝐺 ∈ 𝑆) |
71 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝑋 ∈ 𝐵) |
72 | | cantnfp1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
73 | 72 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝑌 ∈ 𝐴) |
74 | 28 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → (𝐺 supp ∅) ⊆ 𝑋) |
75 | 13, 68, 69, 70, 71, 73, 74, 1 | cantnfp1lem1 8575 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → 𝐹 ∈ 𝑆) |
76 | | onelon 5748 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ On) |
77 | 14, 72, 76 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ On) |
78 | | on0eln0 5780 |
. . . . . 6
⊢ (𝑌 ∈ On → (∅
∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
79 | 77, 78 | syl 17 |
. . . . 5
⊢ (𝜑 → (∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
80 | 79 | biimpar 502 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → ∅ ∈ 𝑌) |
81 | | eqid 2622 |
. . . 4
⊢ OrdIso( E
, (𝐹 supp ∅)) =
OrdIso( E , (𝐹 supp
∅)) |
82 | | eqid 2622 |
. . . 4
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐹 supp
∅))‘𝑘))
·𝑜 (𝐹‘(OrdIso( E , (𝐹 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐹 supp
∅))‘𝑘))
·𝑜 (𝐹‘(OrdIso( E , (𝐹 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
83 | | eqid 2622 |
. . . 4
⊢ OrdIso( E
, (𝐺 supp ∅)) =
OrdIso( E , (𝐺 supp
∅)) |
84 | | eqid 2622 |
. . . 4
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐺 supp
∅))‘𝑘))
·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐺 supp
∅))‘𝑘))
·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
85 | 13, 68, 69, 70, 71, 73, 74, 1, 80, 81, 82, 83, 84 | cantnfp1lem3 8577 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |
86 | 75, 85 | jca 554 |
. 2
⊢ ((𝜑 ∧ 𝑌 ≠ ∅) → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)))) |
87 | 67, 86 | pm2.61dane 2881 |
1
⊢ (𝜑 → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)))) |