Proof of Theorem sucxpdom
| Step | Hyp | Ref
| Expression |
| 1 | | df-suc 6390 |
. 2
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
| 2 | | relsdom 8992 |
. . . . . . . . 9
⊢ Rel
≺ |
| 3 | 2 | brrelex2i 5742 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
| 4 | | 1on 8518 |
. . . . . . . 8
⊢
1o ∈ On |
| 5 | | xpsneng 9096 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 1o
∈ On) → (𝐴
× {1o}) ≈ 𝐴) |
| 6 | 3, 4, 5 | sylancl 586 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → (𝐴 × {1o}) ≈ 𝐴) |
| 7 | 6 | ensymd 9045 |
. . . . . 6
⊢
(1o ≺ 𝐴 → 𝐴 ≈ (𝐴 × {1o})) |
| 8 | | endom 9019 |
. . . . . 6
⊢ (𝐴 ≈ (𝐴 × {1o}) → 𝐴 ≼ (𝐴 × {1o})) |
| 9 | 7, 8 | syl 17 |
. . . . 5
⊢
(1o ≺ 𝐴 → 𝐴 ≼ (𝐴 × {1o})) |
| 10 | | ensn1g 9062 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝐴} ≈
1o) |
| 11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → {𝐴} ≈ 1o) |
| 12 | | ensdomtr 9153 |
. . . . . . . 8
⊢ (({𝐴} ≈ 1o ∧
1o ≺ 𝐴)
→ {𝐴} ≺ 𝐴) |
| 13 | 11, 12 | mpancom 688 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → {𝐴} ≺ 𝐴) |
| 14 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 15 | | xpsneng 9096 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
| 16 | 3, 14, 15 | sylancl 586 |
. . . . . . . 8
⊢
(1o ≺ 𝐴 → (𝐴 × {∅}) ≈ 𝐴) |
| 17 | 16 | ensymd 9045 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → 𝐴 ≈ (𝐴 × {∅})) |
| 18 | | sdomentr 9151 |
. . . . . . 7
⊢ (({𝐴} ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → {𝐴} ≺ (𝐴 × {∅})) |
| 19 | 13, 17, 18 | syl2anc 584 |
. . . . . 6
⊢
(1o ≺ 𝐴 → {𝐴} ≺ (𝐴 × {∅})) |
| 20 | | sdomdom 9020 |
. . . . . 6
⊢ ({𝐴} ≺ (𝐴 × {∅}) → {𝐴} ≼ (𝐴 × {∅})) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢
(1o ≺ 𝐴 → {𝐴} ≼ (𝐴 × {∅})) |
| 22 | | 1n0 8526 |
. . . . . 6
⊢
1o ≠ ∅ |
| 23 | | xpsndisj 6183 |
. . . . . 6
⊢
(1o ≠ ∅ → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
| 24 | 22, 23 | mp1i 13 |
. . . . 5
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
| 25 | | undom 9099 |
. . . . 5
⊢ (((𝐴 ≼ (𝐴 × {1o}) ∧ {𝐴} ≼ (𝐴 × {∅})) ∧ ((𝐴 × {1o}) ∩
(𝐴 × {∅})) =
∅) → (𝐴 ∪
{𝐴}) ≼ ((𝐴 × {1o}) ∪
(𝐴 ×
{∅}))) |
| 26 | 9, 21, 24, 25 | syl21anc 838 |
. . . 4
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) ∪ (𝐴 ×
{∅}))) |
| 27 | | sdomentr 9151 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1o})) →
1o ≺ (𝐴
× {1o})) |
| 28 | 7, 27 | mpdan 687 |
. . . . 5
⊢
(1o ≺ 𝐴 → 1o ≺ (𝐴 ×
{1o})) |
| 29 | | sdomentr 9151 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 1o
≺ (𝐴 ×
{∅})) |
| 30 | 17, 29 | mpdan 687 |
. . . . 5
⊢
(1o ≺ 𝐴 → 1o ≺ (𝐴 ×
{∅})) |
| 31 | | unxpdom 9289 |
. . . . 5
⊢
((1o ≺ (𝐴 × {1o}) ∧
1o ≺ (𝐴
× {∅})) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
| 32 | 28, 30, 31 | syl2anc 584 |
. . . 4
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
| 33 | | domtr 9047 |
. . . 4
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ∧
((𝐴 ×
{1o}) ∪ (𝐴
× {∅})) ≼ ((𝐴 × {1o}) × (𝐴 × {∅}))) →
(𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 ×
{∅}))) |
| 34 | 26, 32, 33 | syl2anc 584 |
. . 3
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 ×
{∅}))) |
| 35 | | xpen 9180 |
. . . 4
⊢ (((𝐴 × {1o})
≈ 𝐴 ∧ (𝐴 × {∅}) ≈
𝐴) → ((𝐴 × {1o})
× (𝐴 ×
{∅})) ≈ (𝐴
× 𝐴)) |
| 36 | 6, 16, 35 | syl2anc 584 |
. . 3
⊢
(1o ≺ 𝐴 → ((𝐴 × {1o}) × (𝐴 × {∅})) ≈
(𝐴 × 𝐴)) |
| 37 | | domentr 9053 |
. . 3
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1o}) × (𝐴 × {∅})) ∧
((𝐴 ×
{1o}) × (𝐴
× {∅})) ≈ (𝐴 × 𝐴)) → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
| 38 | 34, 36, 37 | syl2anc 584 |
. 2
⊢
(1o ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
| 39 | 1, 38 | eqbrtrid 5178 |
1
⊢
(1o ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴)) |