Proof of Theorem cdaassen
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
2 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
3 | | xpsneng 7930 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ∅ ∈ V) → (𝐴 × {∅}) ≈
𝐴) |
4 | 1, 2, 3 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × {∅}) ≈ 𝐴) |
5 | 4 | ensymd 7893 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ (𝐴 × {∅})) |
6 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
7 | | snex 4835 |
. . . . . . . 8
⊢ {∅}
∈ V |
8 | | xpexg 6858 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ {∅} ∈ V) → (𝐵 × {∅}) ∈
V) |
9 | 6, 7, 8 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ∈
V) |
10 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
11 | | xpsneng 7930 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∈ V
∧ 1𝑜 ∈ On) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅})) |
12 | 9, 10, 11 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅})) |
13 | | xpsneng 7930 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ ∅ ∈ V) → (𝐵 × {∅}) ≈
𝐵) |
14 | 6, 2, 13 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ≈ 𝐵) |
15 | | entr 7894 |
. . . . . 6
⊢ ((((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅}) ∧ (𝐵 × {∅}) ≈ 𝐵) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ 𝐵) |
16 | 12, 14, 15 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ 𝐵) |
17 | 16 | ensymd 7893 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ ((𝐵 × {∅}) ×
{1𝑜})) |
18 | | xp01disj 7463 |
. . . . 5
⊢ ((𝐴 × {∅}) ∩
((𝐵 × {∅})
× {1𝑜})) = ∅ |
19 | 18 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∩ ((𝐵 × {∅}) ×
{1𝑜})) = ∅) |
20 | | cdaenun 8879 |
. . . 4
⊢ ((𝐴 ≈ (𝐴 × {∅}) ∧ 𝐵 ≈ ((𝐵 × {∅}) ×
{1𝑜}) ∧ ((𝐴 × {∅}) ∩ ((𝐵 × {∅}) ×
{1𝑜})) = ∅) → (𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜}))) |
21 | 5, 17, 19, 20 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜}))) |
22 | | simp3 1056 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
23 | | snex 4835 |
. . . . . . 7
⊢
{1𝑜} ∈ V |
24 | | xpexg 6858 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ {1𝑜} ∈ V)
→ (𝐶 ×
{1𝑜}) ∈ V) |
25 | 22, 23, 24 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ∈
V) |
26 | | xpsneng 7930 |
. . . . . 6
⊢ (((𝐶 ×
{1𝑜}) ∈ V ∧ 1𝑜 ∈ On) →
((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ (𝐶 ×
{1𝑜})) |
27 | 25, 10, 26 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐶 × {1𝑜}) ×
{1𝑜}) ≈ (𝐶 ×
{1𝑜})) |
28 | | xpsneng 7930 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 1𝑜 ∈ On)
→ (𝐶 ×
{1𝑜}) ≈ 𝐶) |
29 | 22, 10, 28 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ≈
𝐶) |
30 | | entr 7894 |
. . . . 5
⊢ ((((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ (𝐶 ×
{1𝑜}) ∧ (𝐶 × {1𝑜}) ≈
𝐶) → ((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ 𝐶) |
31 | 27, 29, 30 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐶 × {1𝑜}) ×
{1𝑜}) ≈ 𝐶) |
32 | 31 | ensymd 7893 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
33 | | indir 3834 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = (((𝐴 × {∅}) ∩ ((𝐶 ×
{1𝑜}) × {1𝑜})) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
34 | | xp01disj 7463 |
. . . . . 6
⊢ ((𝐴 × {∅}) ∩
((𝐶 ×
{1𝑜}) × {1𝑜})) =
∅ |
35 | | xp01disj 7463 |
. . . . . . . 8
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
36 | 35 | xpeq1i 5059 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) × {1𝑜}) = (∅ ×
{1𝑜}) |
37 | | xpindir 5178 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) × {1𝑜}) = (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
38 | | 0xp 5122 |
. . . . . . 7
⊢ (∅
× {1𝑜}) = ∅ |
39 | 36, 37, 38 | 3eqtr3i 2640 |
. . . . . 6
⊢ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅ |
40 | 34, 39 | uneq12i 3727 |
. . . . 5
⊢ (((𝐴 × {∅}) ∩
((𝐶 ×
{1𝑜}) × {1𝑜})) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜}))) = (∅ ∪ ∅) |
41 | | un0 3919 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
42 | 33, 40, 41 | 3eqtri 2636 |
. . . 4
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅ |
43 | 42 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅) |
44 | | cdaenun 8879 |
. . 3
⊢ (((𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∧ 𝐶 ≈ ((𝐶 × {1𝑜}) ×
{1𝑜}) ∧ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
45 | 21, 32, 43, 44 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
46 | | ovex 6577 |
. . . . 5
⊢ (𝐵 +𝑐 𝐶) ∈ V |
47 | | cdaval 8875 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 +𝑐 𝐶) ∈ V) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜}))) |
48 | 46, 47 | mpan2 703 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜}))) |
49 | | cdaval 8875 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
50 | 49 | xpeq1d 5062 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 +𝑐 𝐶) × {1𝑜}) =
(((𝐵 × {∅})
∪ (𝐶 ×
{1𝑜})) × {1𝑜})) |
51 | | xpundir 5095 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜})) × {1𝑜}) = (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
52 | 50, 51 | syl6eq 2660 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 +𝑐 𝐶) × {1𝑜}) =
(((𝐵 × {∅})
× {1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
53 | 52 | uneq2d 3729 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜})) = ((𝐴 × {∅}) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})))) |
54 | | unass 3732 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ((𝐴 × {∅}) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
55 | 53, 54 | syl6eqr 2662 |
. . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜})) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
56 | 48, 55 | sylan9eq 2664 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋)) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
57 | 56 | 3impb 1252 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
58 | 45, 57 | breqtrrd 4611 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (𝐴 +𝑐 (𝐵 +𝑐 𝐶))) |