Proof of Theorem cda1dif
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . 4
⊢ (𝐴 +𝑐
1𝑜) ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 +𝑐
1𝑜) ∈ V) |
3 | | id 22 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 𝐵 ∈ (𝐴 +𝑐
1𝑜)) |
4 | | df1o2 7459 |
. . . . . . . 8
⊢
1𝑜 = {∅} |
5 | 4 | xpeq1i 5059 |
. . . . . . 7
⊢
(1𝑜 × {1𝑜}) = ({∅}
× {1𝑜}) |
6 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
7 | | 1on 7454 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
8 | 7 | elexi 3186 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
9 | 6, 8 | xpsn 6313 |
. . . . . . 7
⊢
({∅} × {1𝑜}) = {〈∅,
1𝑜〉} |
10 | 5, 9 | eqtri 2632 |
. . . . . 6
⊢
(1𝑜 × {1𝑜}) =
{〈∅, 1𝑜〉} |
11 | | ssun2 3739 |
. . . . . 6
⊢
(1𝑜 × {1𝑜}) ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
12 | 10, 11 | eqsstr3i 3599 |
. . . . 5
⊢
{〈∅, 1𝑜〉} ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
13 | | opex 4859 |
. . . . . 6
⊢
〈∅, 1𝑜〉 ∈ V |
14 | 13 | snss 4259 |
. . . . 5
⊢
(〈∅, 1𝑜〉 ∈ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ↔ {〈∅,
1𝑜〉} ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
15 | 12, 14 | mpbir 220 |
. . . 4
⊢
〈∅, 1𝑜〉 ∈ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
16 | | relxp 5150 |
. . . . . . . 8
⊢ Rel (V
× V) |
17 | | cdafn 8874 |
. . . . . . . . . 10
⊢
+𝑐 Fn (V × V) |
18 | | fndm 5904 |
. . . . . . . . . 10
⊢ (
+𝑐 Fn (V × V) → dom +𝑐 = (V
× V)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
+𝑐 = (V × V) |
20 | 19 | releqi 5125 |
. . . . . . . 8
⊢ (Rel dom
+𝑐 ↔ Rel (V × V)) |
21 | 16, 20 | mpbir 220 |
. . . . . . 7
⊢ Rel dom
+𝑐 |
22 | 21 | ovrcl 6584 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 ∈ V ∧ 1𝑜 ∈
V)) |
23 | 22 | simpld 474 |
. . . . 5
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 𝐴 ∈ V) |
24 | | cdaval 8875 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
25 | 23, 7, 24 | sylancl 693 |
. . . 4
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
26 | 15, 25 | syl5eleqr 2695 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 〈∅, 1𝑜〉 ∈
(𝐴 +𝑐
1𝑜)) |
27 | | difsnen 7927 |
. . 3
⊢ (((𝐴 +𝑐
1𝑜) ∈ V ∧ 𝐵 ∈ (𝐴 +𝑐
1𝑜) ∧ 〈∅, 1𝑜〉 ∈
(𝐴 +𝑐
1𝑜)) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅,
1𝑜〉})) |
28 | 2, 3, 26, 27 | syl3anc 1318 |
. 2
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅,
1𝑜〉})) |
29 | 25 | difeq1d 3689 |
. . . 4
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(((𝐴 × {∅})
∪ (1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉})) |
30 | | xp01disj 7463 |
. . . . . 6
⊢ ((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) =
∅ |
31 | | disj3 3973 |
. . . . . 6
⊢ (((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) = ∅ ↔
(𝐴 × {∅}) =
((𝐴 × {∅})
∖ (1𝑜 ×
{1𝑜}))) |
32 | 30, 31 | mpbi 219 |
. . . . 5
⊢ (𝐴 × {∅}) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
33 | | difun2 4000 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
34 | 10 | difeq2i 3687 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉}) |
35 | 32, 33, 34 | 3eqtr2i 2638 |
. . . 4
⊢ (𝐴 × {∅}) = (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉}) |
36 | 29, 35 | syl6eqr 2662 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(𝐴 ×
{∅})) |
37 | | xpsneng 7930 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
38 | 23, 6, 37 | sylancl 693 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ≈ 𝐴) |
39 | 36, 38 | eqbrtrd 4605 |
. 2
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
≈ 𝐴) |
40 | | entr 7894 |
. 2
⊢ ((((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
∧ ((𝐴
+𝑐 1𝑜) ∖ {〈∅,
1𝑜〉}) ≈ 𝐴) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ 𝐴) |
41 | 28, 39, 40 | syl2anc 691 |
1
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ 𝐴) |