Step | Hyp | Ref
| Expression |
1 | | ralunb 4110 |
. . . . . . 7
⊢
(∀𝑦 ∈
(𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ↔ (∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥))) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐵) → (∀𝑦 ∈ (𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ↔ (∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
3 | 2 | pm5.32da 582 |
. . . . 5
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)) ↔ (𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥))))) |
4 | | anandi 676 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥) ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥))) ↔ ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)) ∧ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
5 | 3, 4 | bitrdi 290 |
. . . 4
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)) ↔ ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)) ∧ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥))))) |
6 | | unss 4103 |
. . . . 5
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) ↔ (𝑋 ∪ 𝑌) ⊆ 𝐵) |
7 | | cntzun.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
8 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
9 | | cntzun.z |
. . . . . 6
⊢ 𝑍 = (Cntz‘𝑀) |
10 | 7, 8, 9 | elcntz 18721 |
. . . . 5
⊢ ((𝑋 ∪ 𝑌) ⊆ 𝐵 → (𝑥 ∈ (𝑍‘(𝑋 ∪ 𝑌)) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
11 | 6, 10 | sylbi 220 |
. . . 4
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑥 ∈ (𝑍‘(𝑋 ∪ 𝑌)) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑋 ∪ 𝑌)(𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
12 | 7, 8, 9 | elcntz 18721 |
. . . . 5
⊢ (𝑋 ⊆ 𝐵 → (𝑥 ∈ (𝑍‘𝑋) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
13 | 7, 8, 9 | elcntz 18721 |
. . . . 5
⊢ (𝑌 ⊆ 𝐵 → (𝑥 ∈ (𝑍‘𝑌) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)))) |
14 | 12, 13 | bi2anan9 639 |
. . . 4
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → ((𝑥 ∈ (𝑍‘𝑋) ∧ 𝑥 ∈ (𝑍‘𝑌)) ↔ ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑋 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥)) ∧ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑌 (𝑥(+g‘𝑀)𝑦) = (𝑦(+g‘𝑀)𝑥))))) |
15 | 5, 11, 14 | 3bitr4d 314 |
. . 3
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑥 ∈ (𝑍‘(𝑋 ∪ 𝑌)) ↔ (𝑥 ∈ (𝑍‘𝑋) ∧ 𝑥 ∈ (𝑍‘𝑌)))) |
16 | | elin 3887 |
. . 3
⊢ (𝑥 ∈ ((𝑍‘𝑋) ∩ (𝑍‘𝑌)) ↔ (𝑥 ∈ (𝑍‘𝑋) ∧ 𝑥 ∈ (𝑍‘𝑌))) |
17 | 15, 16 | bitr4di 292 |
. 2
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑥 ∈ (𝑍‘(𝑋 ∪ 𝑌)) ↔ 𝑥 ∈ ((𝑍‘𝑋) ∩ (𝑍‘𝑌)))) |
18 | 17 | eqrdv 2735 |
1
⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) |