Proof of Theorem sucxpdom
Step | Hyp | Ref
| Expression |
1 | | df-suc 6272 |
. 2
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
2 | | relsdom 8740 |
. . . . . . . . 9
⊢ Rel
≺ |
3 | 2 | brrelex2i 5644 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
4 | | 1on 8309 |
. . . . . . . 8
⊢
1o ∈ On |
5 | | xpsneng 8843 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 1o
∈ On) → (𝐴
× {1o}) ≈ 𝐴) |
6 | 3, 4, 5 | sylancl 586 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → (𝐴 × {1o}) ≈ 𝐴) |
7 | 6 | ensymd 8791 |
. . . . . 6
⊢
(1o ≺ 𝐴 → 𝐴 ≈ (𝐴 × {1o})) |
8 | | endom 8767 |
. . . . . 6
⊢ (𝐴 ≈ (𝐴 × {1o}) → 𝐴 ≼ (𝐴 × {1o})) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢
(1o ≺ 𝐴 → 𝐴 ≼ (𝐴 × {1o})) |
10 | | ensn1g 8809 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝐴} ≈
1o) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → {𝐴} ≈ 1o) |
12 | | ensdomtr 8900 |
. . . . . . . 8
⊢ (({𝐴} ≈ 1o ∧
1o ≺ 𝐴)
→ {𝐴} ≺ 𝐴) |
13 | 11, 12 | mpancom 685 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → {𝐴} ≺ 𝐴) |
14 | | 0ex 5231 |
. . . . . . . . 9
⊢ ∅
∈ V |
15 | | xpsneng 8843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
16 | 3, 14, 15 | sylancl 586 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → (𝐴 × {∅}) ≈ 𝐴) |
17 | 16 | ensymd 8791 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → 𝐴 ≈ (𝐴 × {∅})) |
18 | | sdomentr 8898 |
. . . . . . 7
⊢ (({𝐴} ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → {𝐴} ≺ (𝐴 × {∅})) |
19 | 13, 17, 18 | syl2anc 584 |
. . . . . 6
⊢
(1o ≺ 𝐴 → {𝐴} ≺ (𝐴 × {∅})) |
20 | | sdomdom 8768 |
. . . . . 6
⊢ ({𝐴} ≺ (𝐴 × {∅}) → {𝐴} ≼ (𝐴 × {∅})) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢
(1o ≺ 𝐴 → {𝐴} ≼ (𝐴 × {∅})) |
22 | | 1n0 8318 |
. . . . . 6
⊢
1o ≠ ∅ |
23 | | xpsndisj 6066 |
. . . . . 6
⊢
(1o ≠ ∅ → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
24 | 22, 23 | mp1i 13 |
. . . . 5
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
25 | | undom 8846 |
. . . . 5
⊢ (((𝐴 ≼ (𝐴 × {1o}) ∧ {𝐴} ≼ (𝐴 × {∅})) ∧ ((𝐴 × {1o}) ∩
(𝐴 × {∅})) =
∅) → (𝐴 ∪
{𝐴}) ≼ ((𝐴 × {1o}) ∪
(𝐴 ×
{∅}))) |
26 | 9, 21, 24, 25 | syl21anc 835 |
. . . 4
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) ∪ (𝐴 ×
{∅}))) |
27 | | sdomentr 8898 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1o})) →
1o ≺ (𝐴
× {1o})) |
28 | 7, 27 | mpdan 684 |
. . . . 5
⊢
(1o ≺ 𝐴 → 1o ≺ (𝐴 ×
{1o})) |
29 | | sdomentr 8898 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 1o
≺ (𝐴 ×
{∅})) |
30 | 17, 29 | mpdan 684 |
. . . . 5
⊢
(1o ≺ 𝐴 → 1o ≺ (𝐴 ×
{∅})) |
31 | | unxpdom 9030 |
. . . . 5
⊢
((1o ≺ (𝐴 × {1o}) ∧
1o ≺ (𝐴
× {∅})) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
32 | 28, 30, 31 | syl2anc 584 |
. . . 4
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
33 | | domtr 8793 |
. . . 4
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ∧
((𝐴 ×
{1o}) ∪ (𝐴
× {∅})) ≼ ((𝐴 × {1o}) × (𝐴 × {∅}))) →
(𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 ×
{∅}))) |
34 | 26, 32, 33 | syl2anc 584 |
. . 3
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 ×
{∅}))) |
35 | | xpen 8927 |
. . . 4
⊢ (((𝐴 × {1o})
≈ 𝐴 ∧ (𝐴 × {∅}) ≈
𝐴) → ((𝐴 × {1o})
× (𝐴 ×
{∅})) ≈ (𝐴
× 𝐴)) |
36 | 6, 16, 35 | syl2anc 584 |
. . 3
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) × (𝐴 × {∅})) ≈
(𝐴 × 𝐴)) |
37 | | domentr 8799 |
. . 3
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 × {∅})) ∧
((𝐴 ×
{1o}) × (𝐴
× {∅})) ≈ (𝐴 × 𝐴)) → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
38 | 34, 36, 37 | syl2anc 584 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
39 | 1, 38 | eqbrtrid 5109 |
1
⊢
(1o ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴)) |