Step | Hyp | Ref
| Expression |
1 | | cantnfp1.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → 𝑌 ∈ 𝐴) |
3 | | cantnfp1.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
4 | | cantnfs.s |
. . . . . . . 8
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
5 | | cantnfs.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ On) |
6 | | cantnfs.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ On) |
7 | 4, 5, 6 | cantnfs 8563 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
8 | 3, 7 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
9 | 8 | simpld 475 |
. . . . 5
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
10 | 9 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → (𝐺‘𝑡) ∈ 𝐴) |
11 | 2, 10 | ifcld 4131 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) ∈ 𝐴) |
12 | | cantnfp1.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) |
13 | 11, 12 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
14 | 8 | simprd 479 |
. . . . . 6
⊢ (𝜑 → 𝐺 finSupp ∅) |
15 | 14 | fsuppimpd 8282 |
. . . . 5
⊢ (𝜑 → (𝐺 supp ∅) ∈ Fin) |
16 | | snfi 8038 |
. . . . 5
⊢ {𝑋} ∈ Fin |
17 | | unfi 8227 |
. . . . 5
⊢ (((𝐺 supp ∅) ∈ Fin ∧
{𝑋} ∈ Fin) →
((𝐺 supp ∅) ∪
{𝑋}) ∈
Fin) |
18 | 15, 16, 17 | sylancl 694 |
. . . 4
⊢ (𝜑 → ((𝐺 supp ∅) ∪ {𝑋}) ∈ Fin) |
19 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ 𝐵) |
20 | 19 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘 ∈ 𝐵) |
21 | 1 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌 ∈ 𝐴) |
22 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐺‘𝑘) ∈ V |
23 | | ifexg 4157 |
. . . . . . . 8
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐺‘𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) |
24 | 21, 22, 23 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) |
25 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑡 = 𝑘 → (𝑡 = 𝑋 ↔ 𝑘 = 𝑋)) |
26 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑡 = 𝑘 → (𝐺‘𝑡) = (𝐺‘𝑘)) |
27 | 25, 26 | ifbieq2d 4111 |
. . . . . . . 8
⊢ (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
28 | 27, 12 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝑘 ∈ 𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
29 | 20, 24, 28 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
30 | | eldifn 3733 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
31 | 30 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
32 | | velsn 4193 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋) |
33 | | elun2 3781 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
34 | 32, 33 | sylbir 225 |
. . . . . . . 8
⊢ (𝑘 = 𝑋 → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
35 | 31, 34 | nsyl 135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋) |
36 | 35 | iffalsed 4097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = (𝐺‘𝑘)) |
37 | | ssun1 3776 |
. . . . . . . . 9
⊢ (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) |
38 | | sscon 3744 |
. . . . . . . . 9
⊢ ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)) |
40 | 39 | sseli 3599 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) |
41 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝐺 supp ∅) = (𝐺 supp ∅) |
42 | | eqimss2 3658 |
. . . . . . . . 9
⊢ ((𝐺 supp ∅) = (𝐺 supp ∅) → (𝐺 supp ∅) ⊆ (𝐺 supp ∅)) |
43 | 41, 42 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅)) |
44 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
V) |
46 | 9, 43, 6, 45 | suppssr 7326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑘) = ∅) |
47 | 40, 46 | sylan2 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺‘𝑘) = ∅) |
48 | 29, 36, 47 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = ∅) |
49 | 13, 48 | suppss 7325 |
. . . 4
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})) |
50 | | ssfi 8180 |
. . . 4
⊢ ((((𝐺 supp ∅) ∪ {𝑋}) ∈ Fin ∧ (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})) → (𝐹 supp ∅) ∈ Fin) |
51 | 18, 49, 50 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐹 supp ∅) ∈ Fin) |
52 | 12 | funmpt2 5927 |
. . . . 5
⊢ Fun 𝐹 |
53 | 52 | a1i 11 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
54 | | mptexg 6484 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ∈ V) |
55 | 12, 54 | syl5eqel 2705 |
. . . . 5
⊢ (𝐵 ∈ On → 𝐹 ∈ V) |
56 | 6, 55 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
57 | | funisfsupp 8280 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ ∅ ∈ V) →
(𝐹 finSupp ∅ ↔
(𝐹 supp ∅) ∈
Fin)) |
58 | 53, 56, 45, 57 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝐹 finSupp ∅ ↔ (𝐹 supp ∅) ∈ Fin)) |
59 | 51, 58 | mpbird 247 |
. 2
⊢ (𝜑 → 𝐹 finSupp ∅) |
60 | 4, 5, 6 | cantnfs 8563 |
. 2
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
61 | 13, 59, 60 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐹 ∈ 𝑆) |