Step | Hyp | Ref
| Expression |
1 | | cntzfval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
2 | | cntzfval.p |
. . . . 5
⊢ + =
(+g‘𝑀) |
3 | | cntzfval.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝑀) |
4 | 1, 2, 3 | cntzfval 17753 |
. . . 4
⊢ (𝑀 ∈ V → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) |
5 | 4 | fveq1d 6193 |
. . 3
⊢ (𝑀 ∈ V → (𝑍‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆)) |
6 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝑀)
∈ V |
7 | 1, 6 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
8 | 7 | elpw2 4828 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
9 | | raleq 3138 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥))) |
10 | 9 | rabbidv 3189 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
11 | | eqid 2622 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
12 | 7 | rabex 4813 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ∈ V |
13 | 10, 11, 12 | fvmpt 6282 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
14 | 8, 13 | sylbir 225 |
. . 3
⊢ (𝑆 ⊆ 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
15 | 5, 14 | sylan9eq 2676 |
. 2
⊢ ((𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
16 | | 0fv 6227 |
. . . 4
⊢
(∅‘𝑆) =
∅ |
17 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Cntz‘𝑀) =
∅) |
18 | 3, 17 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝑍 = ∅) |
19 | 18 | fveq1d 6193 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = (∅‘𝑆)) |
20 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ 𝐵 |
21 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑀) =
∅) |
22 | 1, 21 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
23 | 20, 22 | syl5sseq 3653 |
. . . . 5
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅) |
24 | | ss0 3974 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅ → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
26 | 16, 19, 25 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
27 | 26 | adantr 481 |
. 2
⊢ ((¬
𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
28 | 15, 27 | pm2.61ian 831 |
1
⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |