Proof of Theorem cdaassen
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
2 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
3 | | xpsneng 8045 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ∅ ∈ V) → (𝐴 × {∅}) ≈
𝐴) |
4 | 1, 2, 3 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × {∅}) ≈ 𝐴) |
5 | 4 | ensymd 8007 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐴 ≈ (𝐴 × {∅})) |
6 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑊) |
7 | | snex 4908 |
. . . . . . . 8
⊢ {∅}
∈ V |
8 | | xpexg 6960 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ {∅} ∈ V) → (𝐵 × {∅}) ∈
V) |
9 | 6, 7, 8 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ∈
V) |
10 | | 1on 7567 |
. . . . . . 7
⊢
1𝑜 ∈ On |
11 | | xpsneng 8045 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∈ V
∧ 1𝑜 ∈ On) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅})) |
12 | 9, 10, 11 | sylancl 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅})) |
13 | | xpsneng 8045 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ ∅ ∈ V) → (𝐵 × {∅}) ≈
𝐵) |
14 | 6, 2, 13 | sylancl 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 × {∅}) ≈ 𝐵) |
15 | | entr 8008 |
. . . . . 6
⊢ ((((𝐵 × {∅}) ×
{1𝑜}) ≈ (𝐵 × {∅}) ∧ (𝐵 × {∅}) ≈ 𝐵) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ 𝐵) |
16 | 12, 14, 15 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 × {∅}) ×
{1𝑜}) ≈ 𝐵) |
17 | 16 | ensymd 8007 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐵 ≈ ((𝐵 × {∅}) ×
{1𝑜})) |
18 | | xp01disj 7576 |
. . . . 5
⊢ ((𝐴 × {∅}) ∩
((𝐵 × {∅})
× {1𝑜})) = ∅ |
19 | 18 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∩ ((𝐵 × {∅}) ×
{1𝑜})) = ∅) |
20 | | cdaenun 8996 |
. . . 4
⊢ ((𝐴 ≈ (𝐴 × {∅}) ∧ 𝐵 ≈ ((𝐵 × {∅}) ×
{1𝑜}) ∧ ((𝐴 × {∅}) ∩ ((𝐵 × {∅}) ×
{1𝑜})) = ∅) → (𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜}))) |
21 | 5, 17, 19, 20 | syl3anc 1326 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜}))) |
22 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
23 | | snex 4908 |
. . . . . . 7
⊢
{1𝑜} ∈ V |
24 | | xpexg 6960 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ {1𝑜} ∈ V)
→ (𝐶 ×
{1𝑜}) ∈ V) |
25 | 22, 23, 24 | sylancl 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ∈
V) |
26 | | xpsneng 8045 |
. . . . . 6
⊢ (((𝐶 ×
{1𝑜}) ∈ V ∧ 1𝑜 ∈ On) →
((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ (𝐶 ×
{1𝑜})) |
27 | 25, 10, 26 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐶 × {1𝑜}) ×
{1𝑜}) ≈ (𝐶 ×
{1𝑜})) |
28 | | xpsneng 8045 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 1𝑜 ∈ On)
→ (𝐶 ×
{1𝑜}) ≈ 𝐶) |
29 | 22, 10, 28 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐶 × {1𝑜}) ≈
𝐶) |
30 | | entr 8008 |
. . . . 5
⊢ ((((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ (𝐶 ×
{1𝑜}) ∧ (𝐶 × {1𝑜}) ≈
𝐶) → ((𝐶 ×
{1𝑜}) × {1𝑜}) ≈ 𝐶) |
31 | 27, 29, 30 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐶 × {1𝑜}) ×
{1𝑜}) ≈ 𝐶) |
32 | 31 | ensymd 8007 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝐶 ≈ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
33 | | indir 3875 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = (((𝐴 × {∅}) ∩ ((𝐶 ×
{1𝑜}) × {1𝑜})) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
34 | | xp01disj 7576 |
. . . . . 6
⊢ ((𝐴 × {∅}) ∩
((𝐶 ×
{1𝑜}) × {1𝑜})) =
∅ |
35 | | xp01disj 7576 |
. . . . . . . 8
⊢ ((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
36 | 35 | xpeq1i 5135 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) × {1𝑜}) = (∅ ×
{1𝑜}) |
37 | | xpindir 5256 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∩ (𝐶 ×
{1𝑜})) × {1𝑜}) = (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
38 | | 0xp 5199 |
. . . . . . 7
⊢ (∅
× {1𝑜}) = ∅ |
39 | 36, 37, 38 | 3eqtr3i 2652 |
. . . . . 6
⊢ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅ |
40 | 34, 39 | uneq12i 3765 |
. . . . 5
⊢ (((𝐴 × {∅}) ∩
((𝐶 ×
{1𝑜}) × {1𝑜})) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜}))) = (∅ ∪ ∅) |
41 | | un0 3967 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
42 | 33, 40, 41 | 3eqtri 2648 |
. . . 4
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅ |
43 | 42 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅) |
44 | | cdaenun 8996 |
. . 3
⊢ (((𝐴 +𝑐 𝐵) ≈ ((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∧ 𝐶 ≈ ((𝐶 × {1𝑜}) ×
{1𝑜}) ∧ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∩ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ∅) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
45 | 21, 32, 43, 44 | syl3anc 1326 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
46 | | ovex 6678 |
. . . . 5
⊢ (𝐵 +𝑐 𝐶) ∈ V |
47 | | cdaval 8992 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 +𝑐 𝐶) ∈ V) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜}))) |
48 | 46, 47 | mpan2 707 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜}))) |
49 | | cdaval 8992 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐵 +𝑐 𝐶) = ((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
50 | 49 | xpeq1d 5138 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 +𝑐 𝐶) × {1𝑜}) =
(((𝐵 × {∅})
∪ (𝐶 ×
{1𝑜})) × {1𝑜})) |
51 | | xpundir 5172 |
. . . . . . 7
⊢ (((𝐵 × {∅}) ∪ (𝐶 ×
{1𝑜})) × {1𝑜}) = (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})) |
52 | 50, 51 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐵 +𝑐 𝐶) × {1𝑜}) =
(((𝐵 × {∅})
× {1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
53 | 52 | uneq2d 3767 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜})) = ((𝐴 × {∅}) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})))) |
54 | | unass 3770 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
((𝐵 × {∅})
× {1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜})) = ((𝐴 × {∅}) ∪ (((𝐵 × {∅}) ×
{1𝑜}) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
55 | 53, 54 | syl6eqr 2674 |
. . . 4
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 × {∅}) ∪ ((𝐵 +𝑐 𝐶) ×
{1𝑜})) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
56 | 48, 55 | sylan9eq 2676 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋)) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
57 | 56 | 3impb 1260 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 +𝑐 (𝐵 +𝑐 𝐶)) = (((𝐴 × {∅}) ∪ ((𝐵 × {∅}) ×
{1𝑜})) ∪ ((𝐶 × {1𝑜}) ×
{1𝑜}))) |
58 | 45, 57 | breqtrrd 4681 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (𝐴 +𝑐 (𝐵 +𝑐 𝐶))) |