| Step | Hyp | Ref
| Expression |
| 1 | | cntzfval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
| 2 | | cntzfval.p |
. . . . 5
⊢ + =
(+g‘𝑀) |
| 3 | | cntzfval.z |
. . . . 5
⊢ 𝑍 = (Cntz‘𝑀) |
| 4 | 1, 2, 3 | cntzfval 19338 |
. . . 4
⊢ (𝑀 ∈ V → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) |
| 5 | 4 | fveq1d 6908 |
. . 3
⊢ (𝑀 ∈ V → (𝑍‘𝑆) = ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆)) |
| 6 | 1 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 7 | 6 | elpw2 5334 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵) |
| 8 | | raleq 3323 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥) ↔ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥))) |
| 9 | 8 | rabbidv 3444 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 10 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 11 | 6 | rabex 5339 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ∈ V |
| 12 | 9, 10, 11 | fvmpt 7016 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 13 | 7, 12 | sylbir 235 |
. . 3
⊢ (𝑆 ⊆ 𝐵 → ((𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 14 | 5, 13 | sylan9eq 2797 |
. 2
⊢ ((𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 15 | | 0fv 6950 |
. . . 4
⊢
(∅‘𝑆) =
∅ |
| 16 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Cntz‘𝑀) =
∅) |
| 17 | 3, 16 | eqtrid 2789 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝑍 = ∅) |
| 18 | 17 | fveq1d 6908 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = (∅‘𝑆)) |
| 19 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ 𝐵 |
| 20 | | fvprc 6898 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑀) =
∅) |
| 21 | 1, 20 | eqtrid 2789 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
| 22 | 19, 21 | sseqtrid 4026 |
. . . . 5
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅) |
| 23 | | ss0 4402 |
. . . . 5
⊢ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} ⊆ ∅ → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
| 24 | 22, 23 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)} = ∅) |
| 25 | 15, 18, 24 | 3eqtr4a 2803 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 26 | 25 | adantr 480 |
. 2
⊢ ((¬
𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |
| 27 | 14, 26 | pm2.61ian 812 |
1
⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) |