Proof of Theorem infcda1
Step | Hyp | Ref
| Expression |
1 | | reldom 7847 |
. . . . . . . 8
⊢ Rel
≼ |
2 | 1 | brrelex2i 5083 |
. . . . . . 7
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
3 | | 1on 7454 |
. . . . . . 7
⊢
1𝑜 ∈ On |
4 | | cdaval 8875 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
5 | 2, 3, 4 | sylancl 693 |
. . . . . 6
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
6 | | df1o2 7459 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
7 | 6 | xpeq1i 5059 |
. . . . . . . 8
⊢
(1𝑜 × {1𝑜}) = ({∅}
× {1𝑜}) |
8 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
9 | 3 | elexi 3186 |
. . . . . . . . 9
⊢
1𝑜 ∈ V |
10 | 8, 9 | xpsn 6313 |
. . . . . . . 8
⊢
({∅} × {1𝑜}) = {〈∅,
1𝑜〉} |
11 | 7, 10 | eqtr2i 2633 |
. . . . . . 7
⊢
{〈∅, 1𝑜〉} = (1𝑜
× {1𝑜}) |
12 | 11 | a1i 11 |
. . . . . 6
⊢ (ω
≼ 𝐴 →
{〈∅, 1𝑜〉} = (1𝑜 ×
{1𝑜})) |
13 | 5, 12 | difeq12d 3691 |
. . . . 5
⊢ (ω
≼ 𝐴 → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(((𝐴 × {∅})
∪ (1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜}))) |
14 | | difun2 4000 |
. . . . . 6
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
15 | | xp01disj 7463 |
. . . . . . 7
⊢ ((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) =
∅ |
16 | | disj3 3973 |
. . . . . . 7
⊢ (((𝐴 × {∅}) ∩
(1𝑜 × {1𝑜})) = ∅ ↔
(𝐴 × {∅}) =
((𝐴 × {∅})
∖ (1𝑜 ×
{1𝑜}))) |
17 | 15, 16 | mpbi 219 |
. . . . . 6
⊢ (𝐴 × {∅}) = ((𝐴 × {∅}) ∖
(1𝑜 × {1𝑜})) |
18 | 14, 17 | eqtr4i 2635 |
. . . . 5
⊢ (((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜})) ∖
(1𝑜 × {1𝑜})) = (𝐴 × {∅}) |
19 | 13, 18 | syl6eq 2660 |
. . . 4
⊢ (ω
≼ 𝐴 → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉}) =
(𝐴 ×
{∅})) |
20 | | cdadom3 8893 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → 𝐴 ≼ (𝐴 +𝑐
1𝑜)) |
21 | 2, 3, 20 | sylancl 693 |
. . . . . 6
⊢ (ω
≼ 𝐴 → 𝐴 ≼ (𝐴 +𝑐
1𝑜)) |
22 | | domtr 7895 |
. . . . . 6
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐴 +𝑐
1𝑜)) → ω ≼ (𝐴 +𝑐
1𝑜)) |
23 | 21, 22 | mpdan 699 |
. . . . 5
⊢ (ω
≼ 𝐴 → ω
≼ (𝐴
+𝑐 1𝑜)) |
24 | | infdifsn 8437 |
. . . . 5
⊢ (ω
≼ (𝐴
+𝑐 1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
≈ (𝐴
+𝑐 1𝑜)) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (ω
≼ 𝐴 → ((𝐴 +𝑐
1𝑜) ∖ {〈∅, 1𝑜〉})
≈ (𝐴
+𝑐 1𝑜)) |
26 | 19, 25 | eqbrtrrd 4607 |
. . 3
⊢ (ω
≼ 𝐴 → (𝐴 × {∅}) ≈
(𝐴 +𝑐
1𝑜)) |
27 | 26 | ensymd 7893 |
. 2
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐
1𝑜) ≈ (𝐴 × {∅})) |
28 | | xpsneng 7930 |
. . 3
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
29 | 2, 8, 28 | sylancl 693 |
. 2
⊢ (ω
≼ 𝐴 → (𝐴 × {∅}) ≈
𝐴) |
30 | | entr 7894 |
. 2
⊢ (((𝐴 +𝑐
1𝑜) ≈ (𝐴 × {∅}) ∧ (𝐴 × {∅}) ≈ 𝐴) → (𝐴 +𝑐
1𝑜) ≈ 𝐴) |
31 | 27, 29, 30 | syl2anc 691 |
1
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐
1𝑜) ≈ 𝐴) |