Proof of Theorem cda1dif
Step | Hyp | Ref
| Expression |
1 | | ovexd 6680 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 +𝑐
1𝑜) ∈ V) |
2 | | id 22 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 𝐵 ∈ (𝐴 +𝑐
1𝑜)) |
3 | | df1o2 7572 |
. . . . . . . 8
⊢
1𝑜 = {∅} |
4 | 3 | xpeq1i 5135 |
. . . . . . 7
⊢
(1𝑜 × {1𝑜}) = ({∅}
× {1𝑜}) |
5 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
6 | | 1on 7567 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
7 | 6 | elexi 3213 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
8 | 5, 7 | xpsn 6407 |
. . . . . . 7
⊢
({∅} × {1𝑜}) = {〈∅,
1𝑜〉} |
9 | 4, 8 | eqtri 2644 |
. . . . . 6
⊢
(1𝑜 × {1𝑜}) =
{〈∅, 1𝑜〉} |
10 | | ssun2 3777 |
. . . . . 6
⊢
(1𝑜 × {1𝑜}) ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
11 | 9, 10 | eqsstr3i 3636 |
. . . . 5
⊢
{〈∅, 1𝑜〉} ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
12 | | opex 4932 |
. . . . . 6
⊢
〈∅, 1𝑜〉 ∈ V |
13 | 12 | snss 4316 |
. . . . 5
⊢
(〈∅, 1𝑜〉 ∈ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ↔ {〈∅,
1𝑜〉} ⊆ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
14 | 11, 13 | mpbir 221 |
. . . 4
⊢
〈∅, 1𝑜〉 ∈ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) |
15 | | relxp 5227 |
. . . . . . . 8
⊢ Rel (V
× V) |
16 | | cdafn 8991 |
. . . . . . . . . 10
⊢
+𝑐 Fn (V × V) |
17 | | fndm 5990 |
. . . . . . . . . 10
⊢ (
+𝑐 Fn (V × V) → dom +𝑐 = (V
× V)) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
⊢ dom
+𝑐 = (V × V) |
19 | 18 | releqi 5202 |
. . . . . . . 8
⊢ (Rel dom
+𝑐 ↔ Rel (V × V)) |
20 | 15, 19 | mpbir 221 |
. . . . . . 7
⊢ Rel dom
+𝑐 |
21 | 20 | ovrcl 6686 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 ∈ V ∧ 1𝑜 ∈
V)) |
22 | 21 | simpld 475 |
. . . . 5
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 𝐴 ∈ V) |
23 | | cdaval 8992 |
. . . . 5
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
24 | 22, 6, 23 | sylancl 694 |
. . . 4
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
25 | 14, 24 | syl5eleqr 2708 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → 〈∅, 1𝑜〉 ∈
(𝐴 +𝑐
1𝑜)) |
26 | | difsnen 8042 |
. . 3
⊢ (((𝐴 +𝑐
1𝑜) ∈ V ∧ 𝐵 ∈ (𝐴 +𝑐
1𝑜) ∧ 〈∅, 1𝑜〉 ∈
(𝐴 +𝑐
1𝑜)) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅,
1𝑜〉})) |
27 | 1, 2, 25, 26 | syl3anc 1326 |
. 2
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅,
1𝑜〉})) |
28 | 24 | difeq1d 3727 |
. . . 4
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(((𝐴 × {∅})
∪ (1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉})) |
29 | | xp01disj 7576 |
. . . . . 6
⊢ ((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) =
∅ |
30 | | disj3 4021 |
. . . . . 6
⊢ (((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) = ∅ ↔
(𝐴 × {∅}) =
((𝐴 × {∅})
∖ (1𝑜 ×
{1𝑜}))) |
31 | 29, 30 | mpbi 220 |
. . . . 5
⊢ (𝐴 × {∅}) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
32 | | difun2 4048 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
33 | 9 | difeq2i 3725 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉}) |
34 | 31, 32, 33 | 3eqtr2i 2650 |
. . . 4
⊢ (𝐴 × {∅}) = (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
{〈∅, 1𝑜〉}) |
35 | 28, 34 | syl6eqr 2674 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(𝐴 ×
{∅})) |
36 | | xpsneng 8045 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
37 | 22, 5, 36 | sylancl 694 |
. . 3
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ≈ 𝐴) |
38 | 35, 37 | eqbrtrd 4675 |
. 2
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
≈ 𝐴) |
39 | | entr 8008 |
. 2
⊢ ((((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
∧ ((𝐴
+𝑐 1𝑜) ∖ {〈∅,
1𝑜〉}) ≈ 𝐴) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ 𝐴) |
40 | 27, 38, 39 | syl2anc 693 |
1
⊢ (𝐵 ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {𝐵}) ≈ 𝐴) |