Proof of Theorem sucxpdom
Step | Hyp | Ref
| Expression |
1 | | df-suc 5729 |
. 2
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
2 | | relsdom 7962 |
. . . . . . . . 9
⊢ Rel
≺ |
3 | 2 | brrelex2i 5159 |
. . . . . . . 8
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ V) |
4 | | 1on 7567 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
5 | | xpsneng 8045 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → (𝐴 × {1𝑜}) ≈
𝐴) |
6 | 3, 4, 5 | sylancl 694 |
. . . . . . 7
⊢
(1𝑜 ≺ 𝐴 → (𝐴 × {1𝑜}) ≈
𝐴) |
7 | 6 | ensymd 8007 |
. . . . . 6
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ≈ (𝐴 ×
{1𝑜})) |
8 | | endom 7982 |
. . . . . 6
⊢ (𝐴 ≈ (𝐴 × {1𝑜}) →
𝐴 ≼ (𝐴 ×
{1𝑜})) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ≼ (𝐴 ×
{1𝑜})) |
10 | | ensn1g 8021 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → {𝐴} ≈
1𝑜) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
⊢
(1𝑜 ≺ 𝐴 → {𝐴} ≈
1𝑜) |
12 | | ensdomtr 8096 |
. . . . . . . 8
⊢ (({𝐴} ≈ 1𝑜
∧ 1𝑜 ≺ 𝐴) → {𝐴} ≺ 𝐴) |
13 | 11, 12 | mpancom 703 |
. . . . . . 7
⊢
(1𝑜 ≺ 𝐴 → {𝐴} ≺ 𝐴) |
14 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
15 | | xpsneng 8045 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
16 | 3, 14, 15 | sylancl 694 |
. . . . . . . 8
⊢
(1𝑜 ≺ 𝐴 → (𝐴 × {∅}) ≈ 𝐴) |
17 | 16 | ensymd 8007 |
. . . . . . 7
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ≈ (𝐴 × {∅})) |
18 | | sdomentr 8094 |
. . . . . . 7
⊢ (({𝐴} ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → {𝐴} ≺ (𝐴 × {∅})) |
19 | 13, 17, 18 | syl2anc 693 |
. . . . . 6
⊢
(1𝑜 ≺ 𝐴 → {𝐴} ≺ (𝐴 × {∅})) |
20 | | sdomdom 7983 |
. . . . . 6
⊢ ({𝐴} ≺ (𝐴 × {∅}) → {𝐴} ≼ (𝐴 × {∅})) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → {𝐴} ≼ (𝐴 × {∅})) |
22 | | 1n0 7575 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
23 | | xpsndisj 5557 |
. . . . . 6
⊢
(1𝑜 ≠ ∅ → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
24 | 22, 23 | mp1i 13 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
25 | | undom 8048 |
. . . . 5
⊢ (((𝐴 ≼ (𝐴 × {1𝑜}) ∧
{𝐴} ≼ (𝐴 × {∅})) ∧
((𝐴 ×
{1𝑜}) ∩ (𝐴 × {∅})) = ∅) →
(𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
26 | 9, 21, 24, 25 | syl21anc 1325 |
. . . 4
⊢
(1𝑜 ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
27 | | sdomentr 8094 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1𝑜})) →
1𝑜 ≺ (𝐴 ×
{1𝑜})) |
28 | 7, 27 | mpdan 702 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → 1𝑜 ≺ (𝐴 ×
{1𝑜})) |
29 | | sdomentr 8094 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) →
1𝑜 ≺ (𝐴 × {∅})) |
30 | 17, 29 | mpdan 702 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → 1𝑜 ≺ (𝐴 ×
{∅})) |
31 | | unxpdom 8167 |
. . . . 5
⊢
((1𝑜 ≺ (𝐴 × {1𝑜}) ∧
1𝑜 ≺ (𝐴 × {∅})) → ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
32 | 28, 30, 31 | syl2anc 693 |
. . . 4
⊢
(1𝑜 ≺ 𝐴 → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
33 | | domtr 8009 |
. . . 4
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
∧ ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ×
(𝐴 ×
{∅}))) |
34 | 26, 32, 33 | syl2anc 693 |
. . 3
⊢
(1𝑜 ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ×
(𝐴 ×
{∅}))) |
35 | | xpen 8123 |
. . . 4
⊢ (((𝐴 ×
{1𝑜}) ≈ 𝐴 ∧ (𝐴 × {∅}) ≈ 𝐴) → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
36 | 6, 16, 35 | syl2anc 693 |
. . 3
⊢
(1𝑜 ≺ 𝐴 → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
37 | | domentr 8015 |
. . 3
⊢ (((𝐴 ∪ {𝐴}) ≼ ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
∧ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅})) ≈ (𝐴 × 𝐴)) → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
38 | 34, 36, 37 | syl2anc 693 |
. 2
⊢
(1𝑜 ≺ 𝐴 → (𝐴 ∪ {𝐴}) ≼ (𝐴 × 𝐴)) |
39 | 1, 38 | syl5eqbr 4688 |
1
⊢
(1𝑜 ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴)) |