Step | Hyp | Ref
| Expression |
1 | | cntzfval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
2 | | cntzfval.p |
. . . . 5
⊢ + =
(+g‘𝑀) |
3 | | cntzfval.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝑀) |
4 | 1, 2, 3 | cntzfval 17576 |
. . . 4
⊢ (𝑀 ∈ V → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) |
5 | 4 | fveq1d 6105 |
. . 3
⊢ (𝑀 ∈ V → (𝑍‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆)) |
6 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑀)
∈ V |
7 | 1, 6 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
8 | 7 | elpw2 4755 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
9 | | raleq 3115 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥))) |
10 | 9 | rabbidv 3164 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
11 | | eqid 2610 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
12 | 7 | rabex 4740 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ∈ V |
13 | 10, 11, 12 | fvmpt 6191 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
14 | 8, 13 | sylbir 224 |
. . 3
⊢ (𝑆 ⊆ 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
15 | 5, 14 | sylan9eq 2664 |
. 2
⊢ ((𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
16 | | 0fv 6137 |
. . . 4
⊢
(∅‘𝑆) =
∅ |
17 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Cntz‘𝑀) =
∅) |
18 | 3, 17 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝑍 = ∅) |
19 | 18 | fveq1d 6105 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = (∅‘𝑆)) |
20 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ 𝐵 |
21 | | fvprc 6097 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑀) =
∅) |
22 | 1, 21 | syl5eq 2656 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
23 | 20, 22 | syl5sseq 3616 |
. . . . 5
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅) |
24 | | ss0 3926 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅ → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
26 | 16, 19, 25 | 3eqtr4a 2670 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
27 | 26 | adantr 480 |
. 2
⊢ ((¬
𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
28 | 15, 27 | pm2.61ian 827 |
1
⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |