Proof of Theorem ustund
Step | Hyp | Ref
| Expression |
1 | | ustund.3 |
. . 3
⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅) |
2 | | xpco 6186 |
. . 3
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) = ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) = ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵))) |
4 | | xpundi 5651 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) = (((𝐴 ∩ 𝐵) × 𝐴) ∪ ((𝐴 ∩ 𝐵) × 𝐵)) |
5 | | xpindir 5737 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) × 𝐴) = ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) |
6 | | inss1 4164 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) ⊆ (𝐴 × 𝐴) |
7 | | ustund.1 |
. . . . . . 7
⊢ (𝜑 → (𝐴 × 𝐴) ⊆ 𝑉) |
8 | 6, 7 | sstrid 3933 |
. . . . . 6
⊢ (𝜑 → ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) ⊆ 𝑉) |
9 | 5, 8 | eqsstrid 3970 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × 𝐴) ⊆ 𝑉) |
10 | | xpindir 5737 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) × 𝐵) = ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) |
11 | | inss2 4165 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
12 | | ustund.2 |
. . . . . . 7
⊢ (𝜑 → (𝐵 × 𝐵) ⊆ 𝑉) |
13 | 11, 12 | sstrid 3933 |
. . . . . 6
⊢ (𝜑 → ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) ⊆ 𝑉) |
14 | 10, 13 | eqsstrid 3970 |
. . . . 5
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × 𝐵) ⊆ 𝑉) |
15 | 9, 14 | unssd 4121 |
. . . 4
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × 𝐴) ∪ ((𝐴 ∩ 𝐵) × 𝐵)) ⊆ 𝑉) |
16 | 4, 15 | eqsstrid 3970 |
. . 3
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ 𝑉) |
17 | | xpundir 5652 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵)) = ((𝐴 × (𝐴 ∩ 𝐵)) ∪ (𝐵 × (𝐴 ∩ 𝐵))) |
18 | | xpindi 5736 |
. . . . . 6
⊢ (𝐴 × (𝐴 ∩ 𝐵)) = ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) |
19 | | inss1 4164 |
. . . . . . 7
⊢ ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐴) |
20 | 19, 7 | sstrid 3933 |
. . . . . 6
⊢ (𝜑 → ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) ⊆ 𝑉) |
21 | 18, 20 | eqsstrid 3970 |
. . . . 5
⊢ (𝜑 → (𝐴 × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
22 | | xpindi 5736 |
. . . . . 6
⊢ (𝐵 × (𝐴 ∩ 𝐵)) = ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) |
23 | | inss2 4165 |
. . . . . . 7
⊢ ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
24 | 23, 12 | sstrid 3933 |
. . . . . 6
⊢ (𝜑 → ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) ⊆ 𝑉) |
25 | 22, 24 | eqsstrid 3970 |
. . . . 5
⊢ (𝜑 → (𝐵 × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
26 | 21, 25 | unssd 4121 |
. . . 4
⊢ (𝜑 → ((𝐴 × (𝐴 ∩ 𝐵)) ∪ (𝐵 × (𝐴 ∩ 𝐵))) ⊆ 𝑉) |
27 | 17, 26 | eqsstrid 3970 |
. . 3
⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
28 | 16, 27 | coss12d 14627 |
. 2
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) ⊆ (𝑉 ∘ 𝑉)) |
29 | 3, 28 | eqsstrrd 3961 |
1
⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ (𝑉 ∘ 𝑉)) |