Proof of Theorem cantnfrescl
Step | Hyp | Ref
| Expression |
1 | | cantnfrescl.b |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝐷) |
2 | | cantnfrescl.x |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅) |
3 | | cantnfrescl.a |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈ 𝐴) |
4 | 3 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → ∅ ∈ 𝐴) |
5 | 2, 4 | eqeltrd 2907 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 ∈ 𝐴) |
6 | 5 | ralrimiva 3176 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ (𝐷 ∖ 𝐵)𝑋 ∈ 𝐴) |
7 | 1, 6 | raldifeq 4282 |
. . . 4
⊢ (𝜑 → (∀𝑛 ∈ 𝐵 𝑋 ∈ 𝐴 ↔ ∀𝑛 ∈ 𝐷 𝑋 ∈ 𝐴)) |
8 | | eqid 2826 |
. . . . 5
⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋) |
9 | 8 | fmpt 6630 |
. . . 4
⊢
(∀𝑛 ∈
𝐵 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴) |
10 | | eqid 2826 |
. . . . 5
⊢ (𝑛 ∈ 𝐷 ↦ 𝑋) = (𝑛 ∈ 𝐷 ↦ 𝑋) |
11 | 10 | fmpt 6630 |
. . . 4
⊢
(∀𝑛 ∈
𝐷 𝑋 ∈ 𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴) |
12 | 7, 9, 11 | 3bitr3g 305 |
. . 3
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴)) |
13 | | cantnfs.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ On) |
14 | | mptexg 6741 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V) |
16 | | funmpt 6162 |
. . . . . 6
⊢ Fun
(𝑛 ∈ 𝐵 ↦ 𝑋) |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) |
18 | | cantnfrescl.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ On) |
19 | | mptexg 6741 |
. . . . . . 7
⊢ (𝐷 ∈ On → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V) |
21 | | funmpt 6162 |
. . . . . 6
⊢ Fun
(𝑛 ∈ 𝐷 ↦ 𝑋) |
22 | 20, 21 | jctir 518 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋))) |
23 | 15, 17, 22 | jca31 512 |
. . . 4
⊢ (𝜑 → (((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) ∧ ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋)))) |
24 | 18, 1, 2 | extmptsuppeq 7584 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) |
25 | | suppeqfsuppbi 8559 |
. . . 4
⊢ ((((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐵 ↦ 𝑋)) ∧ ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ V ∧ Fun (𝑛 ∈ 𝐷 ↦ 𝑋))) → (((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅) → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅))) |
26 | 23, 24, 25 | sylc 65 |
. . 3
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅ ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅)) |
27 | 12, 26 | anbi12d 626 |
. 2
⊢ (𝜑 → (((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅) ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅))) |
28 | | cantnfs.s |
. . 3
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
29 | | cantnfs.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
30 | 28, 29, 13 | cantnfs 8841 |
. 2
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ ((𝑛 ∈ 𝐵 ↦ 𝑋):𝐵⟶𝐴 ∧ (𝑛 ∈ 𝐵 ↦ 𝑋) finSupp ∅))) |
31 | | cantnfrescl.t |
. . 3
⊢ 𝑇 = dom (𝐴 CNF 𝐷) |
32 | 31, 29, 18 | cantnfs 8841 |
. 2
⊢ (𝜑 → ((𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇 ↔ ((𝑛 ∈ 𝐷 ↦ 𝑋):𝐷⟶𝐴 ∧ (𝑛 ∈ 𝐷 ↦ 𝑋) finSupp ∅))) |
33 | 27, 30, 32 | 3bitr4d 303 |
1
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇)) |