Step | Hyp | Ref
| Expression |
1 | | cntzfval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
2 | | cntzfval.p |
. . . . 5
⊢ + =
(+g‘𝑀) |
3 | | cntzfval.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝑀) |
4 | 1, 2, 3 | cntzfval 18714 |
. . . 4
⊢ (𝑀 ∈ V → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) |
5 | 4 | fveq1d 6719 |
. . 3
⊢ (𝑀 ∈ V → (𝑍‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆)) |
6 | 1 | fvexi 6731 |
. . . . 5
⊢ 𝐵 ∈ V |
7 | 6 | elpw2 5238 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
8 | | raleq 3319 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥))) |
9 | 8 | rabbidv 3390 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
10 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
11 | 6 | rabex 5225 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ∈ V |
12 | 9, 10, 11 | fvmpt 6818 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
13 | 7, 12 | sylbir 238 |
. . 3
⊢ (𝑆 ⊆ 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
14 | 5, 13 | sylan9eq 2798 |
. 2
⊢ ((𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
15 | | 0fv 6756 |
. . . 4
⊢
(∅‘𝑆) =
∅ |
16 | | fvprc 6709 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Cntz‘𝑀) =
∅) |
17 | 3, 16 | syl5eq 2790 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝑍 = ∅) |
18 | 17 | fveq1d 6719 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = (∅‘𝑆)) |
19 | | ssrab2 3993 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ 𝐵 |
20 | | fvprc 6709 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑀) =
∅) |
21 | 1, 20 | syl5eq 2790 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
22 | 19, 21 | sseqtrid 3953 |
. . . . 5
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅) |
23 | | ss0 4313 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅ → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
25 | 15, 18, 24 | 3eqtr4a 2804 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
26 | 25 | adantr 484 |
. 2
⊢ ((¬
𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
27 | 14, 26 | pm2.61ian 812 |
1
⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |