Proof of Theorem cdaen
Step | Hyp | Ref
| Expression |
1 | | relen 7960 |
. . . . . 6
⊢ Rel
≈ |
2 | 1 | brrelexi 5158 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → 𝐴 ∈ V) |
3 | | 0ex 4790 |
. . . . 5
⊢ ∅
∈ V |
4 | | xpsneng 8045 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
5 | 2, 3, 4 | sylancl 694 |
. . . 4
⊢ (𝐴 ≈ 𝐵 → (𝐴 × {∅}) ≈ 𝐴) |
6 | 1 | brrelex2i 5159 |
. . . . . . 7
⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V) |
7 | | xpsneng 8045 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ ∅ ∈
V) → (𝐵 ×
{∅}) ≈ 𝐵) |
8 | 6, 3, 7 | sylancl 694 |
. . . . . 6
⊢ (𝐴 ≈ 𝐵 → (𝐵 × {∅}) ≈ 𝐵) |
9 | 8 | ensymd 8007 |
. . . . 5
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ (𝐵 × {∅})) |
10 | | entr 8008 |
. . . . 5
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ (𝐵 × {∅})) → 𝐴 ≈ (𝐵 × {∅})) |
11 | 9, 10 | mpdan 702 |
. . . 4
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≈ (𝐵 × {∅})) |
12 | | entr 8008 |
. . . 4
⊢ (((𝐴 × {∅}) ≈
𝐴 ∧ 𝐴 ≈ (𝐵 × {∅})) → (𝐴 × {∅}) ≈
(𝐵 ×
{∅})) |
13 | 5, 11, 12 | syl2anc 693 |
. . 3
⊢ (𝐴 ≈ 𝐵 → (𝐴 × {∅}) ≈ (𝐵 ×
{∅})) |
14 | 1 | brrelexi 5158 |
. . . . 5
⊢ (𝐶 ≈ 𝐷 → 𝐶 ∈ V) |
15 | | 1on 7567 |
. . . . 5
⊢
1𝑜 ∈ On |
16 | | xpsneng 8045 |
. . . . 5
⊢ ((𝐶 ∈ V ∧
1𝑜 ∈ On) → (𝐶 × {1𝑜}) ≈
𝐶) |
17 | 14, 15, 16 | sylancl 694 |
. . . 4
⊢ (𝐶 ≈ 𝐷 → (𝐶 × {1𝑜}) ≈
𝐶) |
18 | 1 | brrelex2i 5159 |
. . . . . . 7
⊢ (𝐶 ≈ 𝐷 → 𝐷 ∈ V) |
19 | | xpsneng 8045 |
. . . . . . 7
⊢ ((𝐷 ∈ V ∧
1𝑜 ∈ On) → (𝐷 × {1𝑜}) ≈
𝐷) |
20 | 18, 15, 19 | sylancl 694 |
. . . . . 6
⊢ (𝐶 ≈ 𝐷 → (𝐷 × {1𝑜}) ≈
𝐷) |
21 | 20 | ensymd 8007 |
. . . . 5
⊢ (𝐶 ≈ 𝐷 → 𝐷 ≈ (𝐷 ×
{1𝑜})) |
22 | | entr 8008 |
. . . . 5
⊢ ((𝐶 ≈ 𝐷 ∧ 𝐷 ≈ (𝐷 × {1𝑜})) →
𝐶 ≈ (𝐷 ×
{1𝑜})) |
23 | 21, 22 | mpdan 702 |
. . . 4
⊢ (𝐶 ≈ 𝐷 → 𝐶 ≈ (𝐷 ×
{1𝑜})) |
24 | | entr 8008 |
. . . 4
⊢ (((𝐶 ×
{1𝑜}) ≈ 𝐶 ∧ 𝐶 ≈ (𝐷 × {1𝑜})) →
(𝐶 ×
{1𝑜}) ≈ (𝐷 ×
{1𝑜})) |
25 | 17, 23, 24 | syl2anc 693 |
. . 3
⊢ (𝐶 ≈ 𝐷 → (𝐶 × {1𝑜}) ≈
(𝐷 ×
{1𝑜})) |
26 | | xp01disj 7576 |
. . . 4
⊢ ((𝐴 × {∅}) ∩ (𝐶 ×
{1𝑜})) = ∅ |
27 | | xp01disj 7576 |
. . . 4
⊢ ((𝐵 × {∅}) ∩ (𝐷 ×
{1𝑜})) = ∅ |
28 | | unen 8040 |
. . . 4
⊢ ((((𝐴 × {∅}) ≈
(𝐵 × {∅}) ∧
(𝐶 ×
{1𝑜}) ≈ (𝐷 × {1𝑜})) ∧
(((𝐴 × {∅})
∩ (𝐶 ×
{1𝑜})) = ∅ ∧ ((𝐵 × {∅}) ∩ (𝐷 × {1𝑜})) =
∅)) → ((𝐴
× {∅}) ∪ (𝐶
× {1𝑜})) ≈ ((𝐵 × {∅}) ∪ (𝐷 ×
{1𝑜}))) |
29 | 26, 27, 28 | mpanr12 721 |
. . 3
⊢ (((𝐴 × {∅}) ≈
(𝐵 × {∅}) ∧
(𝐶 ×
{1𝑜}) ≈ (𝐷 × {1𝑜})) →
((𝐴 × {∅})
∪ (𝐶 ×
{1𝑜})) ≈ ((𝐵 × {∅}) ∪ (𝐷 ×
{1𝑜}))) |
30 | 13, 25, 29 | syl2an 494 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → ((𝐴 × {∅}) ∪ (𝐶 × {1𝑜})) ≈
((𝐵 × {∅})
∪ (𝐷 ×
{1𝑜}))) |
31 | | cdaval 8992 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 +𝑐 𝐶) = ((𝐴 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
32 | 2, 14, 31 | syl2an 494 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 +𝑐 𝐶) = ((𝐴 × {∅}) ∪ (𝐶 ×
{1𝑜}))) |
33 | | cdaval 8992 |
. . 3
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → (𝐵 +𝑐 𝐷) = ((𝐵 × {∅}) ∪ (𝐷 ×
{1𝑜}))) |
34 | 6, 18, 33 | syl2an 494 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐵 +𝑐 𝐷) = ((𝐵 × {∅}) ∪ (𝐷 ×
{1𝑜}))) |
35 | 30, 32, 34 | 3brtr4d 4685 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 +𝑐 𝐶) ≈ (𝐵 +𝑐 𝐷)) |