Proof of Theorem ustund
Step | Hyp | Ref
| Expression |
1 | | ustund.3 |
. . 3
⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅) |
2 | | xpco 5675 |
. . 3
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) = ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) = ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵))) |
4 | | xpundir 5172 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵)) = ((𝐴 × (𝐴 ∩ 𝐵)) ∪ (𝐵 × (𝐴 ∩ 𝐵))) |
5 | | xpindi 5255 |
. . . . . . 7
⊢ (𝐴 × (𝐴 ∩ 𝐵)) = ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) |
6 | | inss1 3833 |
. . . . . . . 8
⊢ ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐴) |
7 | | ustund.1 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × 𝐴) ⊆ 𝑉) |
8 | 6, 7 | syl5ss 3614 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × 𝐴) ∩ (𝐴 × 𝐵)) ⊆ 𝑉) |
9 | 5, 8 | syl5eqss 3649 |
. . . . . 6
⊢ (𝜑 → (𝐴 × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
10 | | xpindi 5255 |
. . . . . . 7
⊢ (𝐵 × (𝐴 ∩ 𝐵)) = ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) |
11 | | inss2 3834 |
. . . . . . . 8
⊢ ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
12 | | ustund.2 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 × 𝐵) ⊆ 𝑉) |
13 | 11, 12 | syl5ss 3614 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 × 𝐴) ∩ (𝐵 × 𝐵)) ⊆ 𝑉) |
14 | 10, 13 | syl5eqss 3649 |
. . . . . 6
⊢ (𝜑 → (𝐵 × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
15 | 9, 14 | unssd 3789 |
. . . . 5
⊢ (𝜑 → ((𝐴 × (𝐴 ∩ 𝐵)) ∪ (𝐵 × (𝐴 ∩ 𝐵))) ⊆ 𝑉) |
16 | 4, 15 | syl5eqss 3649 |
. . . 4
⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵)) ⊆ 𝑉) |
17 | | coss2 5278 |
. . . 4
⊢ (((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵)) ⊆ 𝑉 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) ⊆ (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ 𝑉)) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) ⊆ (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ 𝑉)) |
19 | | xpundi 5171 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) = (((𝐴 ∩ 𝐵) × 𝐴) ∪ ((𝐴 ∩ 𝐵) × 𝐵)) |
20 | | xpindir 5256 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) × 𝐴) = ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) |
21 | | inss1 3833 |
. . . . . . . 8
⊢ ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) ⊆ (𝐴 × 𝐴) |
22 | 21, 7 | syl5ss 3614 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × 𝐴) ∩ (𝐵 × 𝐴)) ⊆ 𝑉) |
23 | 20, 22 | syl5eqss 3649 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × 𝐴) ⊆ 𝑉) |
24 | | xpindir 5256 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) × 𝐵) = ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) |
25 | | inss2 3834 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
26 | 25, 12 | syl5ss 3614 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × 𝐵) ∩ (𝐵 × 𝐵)) ⊆ 𝑉) |
27 | 24, 26 | syl5eqss 3649 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × 𝐵) ⊆ 𝑉) |
28 | 23, 27 | unssd 3789 |
. . . . 5
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × 𝐴) ∪ ((𝐴 ∩ 𝐵) × 𝐵)) ⊆ 𝑉) |
29 | 19, 28 | syl5eqss 3649 |
. . . 4
⊢ (𝜑 → ((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ 𝑉) |
30 | | coss1 5277 |
. . . 4
⊢ (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ 𝑉 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ 𝑉) ⊆ (𝑉 ∘ 𝑉)) |
31 | 29, 30 | syl 17 |
. . 3
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ 𝑉) ⊆ (𝑉 ∘ 𝑉)) |
32 | 18, 31 | sstrd 3613 |
. 2
⊢ (𝜑 → (((𝐴 ∩ 𝐵) × (𝐴 ∪ 𝐵)) ∘ ((𝐴 ∪ 𝐵) × (𝐴 ∩ 𝐵))) ⊆ (𝑉 ∘ 𝑉)) |
33 | 3, 32 | eqsstr3d 3640 |
1
⊢ (𝜑 → ((𝐴 ∪ 𝐵) × (𝐴 ∪ 𝐵)) ⊆ (𝑉 ∘ 𝑉)) |