Proof of Theorem xpcdaen
Step | Hyp | Ref
| Expression |
1 | | enrefg 7873 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
2 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ 𝐴) |
3 | | simp2 1055 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
4 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
5 | | xpsneng 7930 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ ∅ ∈ V) → (𝐵 × {∅}) ≈
𝐵) |
6 | 3, 4, 5 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ≈ 𝐵) |
7 | 6 | ensymd 7893 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ (𝐵 × {∅})) |
8 | | xpen 8008 |
. . . . 5
⊢ ((𝐴 ≈ 𝐴 ∧ 𝐵 ≈ (𝐵 × {∅})) → (𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅}))) |
9 | 2, 7, 8 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅}))) |
10 | | simp3 1056 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
11 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
12 | | xpsneng 7930 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 1𝑜 ∈ On)
→ (𝐶 ×
{1𝑜}) ≈ 𝐶) |
13 | 10, 11, 12 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ≈
𝐶) |
14 | 13 | ensymd 7893 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ (𝐶 ×
{1𝑜})) |
15 | | xpen 8008 |
. . . . 5
⊢ ((𝐴 ≈ 𝐴 ∧ 𝐶 ≈ (𝐶 × {1𝑜})) →
(𝐴 × 𝐶) ≈ (𝐴 × (𝐶 ×
{1𝑜}))) |
16 | 2, 14, 15 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × 𝐶) ≈ (𝐴 × (𝐶 ×
{1𝑜}))) |
17 | | xp01disj 7463 |
. . . . . . 7
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
18 | 17 | xpeq2i 5060 |
. . . . . 6
⊢ (𝐴 × ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜}))) = (𝐴 ×
∅) |
19 | | xpindi 5177 |
. . . . . 6
⊢ (𝐴 × ((𝐵 × {∅}) ∩ (𝐶 × {1𝑜}))) =
((𝐴 × (𝐵 × {∅})) ∩
(𝐴 × (𝐶 ×
{1𝑜}))) |
20 | | xp0 5471 |
. . . . . 6
⊢ (𝐴 × ∅) =
∅ |
21 | 18, 19, 20 | 3eqtr3i 2640 |
. . . . 5
⊢ ((𝐴 × (𝐵 × {∅})) ∩ (𝐴 × (𝐶 × {1𝑜}))) =
∅ |
22 | 21 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × (𝐵 × {∅})) ∩ (𝐴 × (𝐶 × {1𝑜}))) =
∅) |
23 | | cdaenun 8879 |
. . . 4
⊢ (((𝐴 × 𝐵) ≈ (𝐴 × (𝐵 × {∅})) ∧ (𝐴 × 𝐶) ≈ (𝐴 × (𝐶 × {1𝑜})) ∧
((𝐴 × (𝐵 × {∅})) ∩
(𝐴 × (𝐶 ×
{1𝑜}))) = ∅) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
24 | 9, 16, 22, 23 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
25 | | cdaval 8875 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
26 | 25 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
27 | 26 | xpeq2d 5063 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) = (𝐴 × ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜})))) |
28 | | xpundi 5094 |
. . . 4
⊢ (𝐴 × ((𝐵 × {∅}) ∪ (𝐶 × {1𝑜}))) =
((𝐴 × (𝐵 × {∅})) ∪
(𝐴 × (𝐶 ×
{1𝑜}))) |
29 | 27, 28 | syl6eq 2660 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) = ((𝐴 × (𝐵 × {∅})) ∪ (𝐴 × (𝐶 ×
{1𝑜})))) |
30 | 24, 29 | breqtrrd 4611 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)) ≈ (𝐴 × (𝐵 +𝑐 𝐶))) |
31 | 30 | ensymd 7893 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) ≈ ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶))) |