Proof of Theorem xpcdaen
Step | Hyp | Ref
| Expression |
1 | | enrefg 7987 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
2 | 1 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ 𝐴) |
3 | | simp2 1062 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
4 | | 0ex 4790 |
. . . . . . 7
⊢ ∅
∈ V |
5 | | xpsneng 8045 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ ∅ ∈ V) → (𝐵 × {∅}) ≈
𝐵) |
6 | 3, 4, 5 | sylancl 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ≈ 𝐵) |
7 | 6 | ensymd 8007 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ (𝐵 × {∅})) |
8 | | xpen 8123 |
. . . . 5
⊢ ((𝐴 ≈ 𝐴 ∧ 𝐵 ≈ (𝐵 × {∅})) → (𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅}))) |
9 | 2, 7, 8 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅}))) |
10 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
11 | | 1on 7567 |
. . . . . . 7
⊢
1𝑜 ∈ On |
12 | | xpsneng 8045 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 1𝑜 ∈ On)
→ (𝐶 ×
{1𝑜}) ≈ 𝐶) |
13 | 10, 11, 12 | sylancl 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ≈
𝐶) |
14 | 13 | ensymd 8007 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ (𝐶 ×
{1𝑜})) |
15 | | xpen 8123 |
. . . . 5
⊢ ((𝐴 ≈ 𝐴 ∧ 𝐶 ≈ (𝐶 × {1𝑜})) →
(𝐴 × 𝐶) ≈ (𝐴 × (𝐶 ×
{1𝑜}))) |
16 | 2, 14, 15 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × 𝐶) ≈ (𝐴 × (𝐶 ×
{1𝑜}))) |
17 | | xp01disj 7576 |
. . . . . . 7
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
18 | 17 | xpeq2i 5136 |
. . . . . 6
⊢ (𝐴 × ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜}))) = (𝐴 ×
∅) |
19 | | xpindi 5255 |
. . . . . 6
⊢ (𝐴 × ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜}))) =
((𝐴 × (𝐵 × {∅})) ∩
(𝐴 × (𝐶 ×
{1𝑜}))) |
20 | | xp0 5552 |
. . . . . 6
⊢ (𝐴 × ∅) =
∅ |
21 | 18, 19, 20 | 3eqtr3i 2652 |
. . . . 5
⊢ ((𝐴 × (𝐵 × {∅})) ∩ (𝐴 × (𝐶 × {1𝑜}))) =
∅ |
22 | 21 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × (𝐵 × {∅})) ∩ (𝐴 × (𝐶 × {1𝑜}))) =
∅) |
23 | | cdaenun 8996 |
. . . 4
⊢ (((𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅})) ∧ (𝐴 × 𝐶) ≈ (𝐴 × (𝐶 × {1𝑜})) ∧
((𝐴 × (𝐵 × {∅})) ∩
(𝐴 × (𝐶 ×
{1𝑜}))) = ∅) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
24 | 9, 16, 22, 23 | syl3anc 1326 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
25 | | cdaval 8992 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
26 | 25 | 3adant1 1079 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
27 | 26 | xpeq2d 5139 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) = (𝐴 × ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜})))) |
28 | | xpundi 5171 |
. . . 4
⊢ (𝐴 × ((𝐵 × {∅}) ∪ (𝐶 × {1𝑜}))) =
((𝐴 × (𝐵 × {∅})) ∪
(𝐴 × (𝐶 ×
{1𝑜}))) |
29 | 27, 28 | syl6eq 2672 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) = ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
30 | 24, 29 | breqtrrd 4681 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ (𝐴 × (𝐵 +𝑐 𝐶))) |
31 | 30 | ensymd 8007 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) ≈ ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶))) |