Proof of Theorem eqrelrel
Step | Hyp | Ref
| Expression |
1 | | unss 3301 |
. 2
⊢ ((𝐴 ⊆ ((V × V) ×
V) ∧ 𝐵 ⊆ ((V
× V) × V)) ↔ (𝐴 ∪ 𝐵) ⊆ ((V × V) ×
V)) |
2 | | ssrelrel 4709 |
. . . 4
⊢ (𝐴 ⊆ ((V × V) ×
V) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) |
3 | | ssrelrel 4709 |
. . . 4
⊢ (𝐵 ⊆ ((V × V) ×
V) → (𝐵 ⊆ 𝐴 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴))) |
4 | 2, 3 | bi2anan9 601 |
. . 3
⊢ ((𝐴 ⊆ ((V × V) ×
V) ∧ 𝐵 ⊆ ((V
× V) × V)) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴)))) |
5 | | eqss 3162 |
. . 3
⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) |
6 | | 2albiim 1481 |
. . . . 5
⊢
(∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ↔ (∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴))) |
7 | 6 | albii 1463 |
. . . 4
⊢
(∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ↔ ∀𝑥(∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴))) |
8 | | 19.26 1474 |
. . . 4
⊢
(∀𝑥(∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴)) ↔ (∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴))) |
9 | 7, 8 | bitri 183 |
. . 3
⊢
(∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ↔ (∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵 → 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴))) |
10 | 4, 5, 9 | 3bitr4g 222 |
. 2
⊢ ((𝐴 ⊆ ((V × V) ×
V) ∧ 𝐵 ⊆ ((V
× V) × V)) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) |
11 | 1, 10 | sylbir 134 |
1
⊢ ((𝐴 ∪ 𝐵) ⊆ ((V × V) × V) →
(𝐴 = 𝐵 ↔ ∀𝑥∀𝑦∀𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐴 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 ∈ 𝐵))) |