Proof of Theorem unxpdom2
Step | Hyp | Ref
| Expression |
1 | | relsdom 8638 |
. . . . . . . 8
⊢ Rel
≺ |
2 | 1 | brrelex2i 5611 |
. . . . . . 7
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
3 | 2 | adantr 484 |
. . . . . 6
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
4 | | 1onn 8372 |
. . . . . 6
⊢
1o ∈ ω |
5 | | xpsneng 8735 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 1o
∈ ω) → (𝐴
× {1o}) ≈ 𝐴) |
6 | 3, 4, 5 | sylancl 589 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {1o}) ≈ 𝐴) |
7 | 6 | ensymd 8684 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 × {1o})) |
8 | | endom 8660 |
. . . 4
⊢ (𝐴 ≈ (𝐴 × {1o}) → 𝐴 ≼ (𝐴 × {1o})) |
9 | 7, 8 | syl 17 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≼ (𝐴 × {1o})) |
10 | | simpr 488 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ 𝐴) |
11 | | 0ex 5205 |
. . . . . 6
⊢ ∅
∈ V |
12 | | xpsneng 8735 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
13 | 3, 11, 12 | sylancl 589 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {∅}) ≈ 𝐴) |
14 | 13 | ensymd 8684 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 × {∅})) |
15 | | domentr 8692 |
. . . 4
⊢ ((𝐵 ≼ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 𝐵 ≼ (𝐴 × {∅})) |
16 | 10, 14, 15 | syl2anc 587 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ (𝐴 × {∅})) |
17 | | 1n0 8226 |
. . . 4
⊢
1o ≠ ∅ |
18 | | xpsndisj 6031 |
. . . 4
⊢
(1o ≠ ∅ → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
19 | 17, 18 | mp1i 13 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1o}) ∩ (𝐴 × {∅})) =
∅) |
20 | | undom 8738 |
. . 3
⊢ (((𝐴 ≼ (𝐴 × {1o}) ∧ 𝐵 ≼ (𝐴 × {∅})) ∧ ((𝐴 × {1o}) ∩
(𝐴 × {∅})) =
∅) → (𝐴 ∪
𝐵) ≼ ((𝐴 × {1o}) ∪
(𝐴 ×
{∅}))) |
21 | 9, 16, 19, 20 | syl21anc 838 |
. 2
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ ((𝐴 × {1o}) ∪ (𝐴 ×
{∅}))) |
22 | | sdomentr 8785 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1o})) →
1o ≺ (𝐴
× {1o})) |
23 | 7, 22 | syldan 594 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1o ≺ (𝐴 ×
{1o})) |
24 | | sdomentr 8785 |
. . . . 5
⊢
((1o ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 1o
≺ (𝐴 ×
{∅})) |
25 | 14, 24 | syldan 594 |
. . . 4
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1o ≺ (𝐴 ×
{∅})) |
26 | | unxpdom 8890 |
. . . 4
⊢
((1o ≺ (𝐴 × {1o}) ∧
1o ≺ (𝐴
× {∅})) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
27 | 23, 25, 26 | syl2anc 587 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
((𝐴 ×
{1o}) × (𝐴
× {∅}))) |
28 | | xpen 8814 |
. . . 4
⊢ (((𝐴 × {1o})
≈ 𝐴 ∧ (𝐴 × {∅}) ≈
𝐴) → ((𝐴 × {1o})
× (𝐴 ×
{∅})) ≈ (𝐴
× 𝐴)) |
29 | 6, 13, 28 | syl2anc 587 |
. . 3
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1o}) × (𝐴 × {∅})) ≈
(𝐴 × 𝐴)) |
30 | | domentr 8692 |
. . 3
⊢ ((((𝐴 × {1o}) ∪
(𝐴 × {∅}))
≼ ((𝐴 ×
{1o}) × (𝐴
× {∅})) ∧ ((𝐴 × {1o}) × (𝐴 × {∅})) ≈
(𝐴 × 𝐴)) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
(𝐴 × 𝐴)) |
31 | 27, 29, 30 | syl2anc 587 |
. 2
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ≼
(𝐴 × 𝐴)) |
32 | | domtr 8686 |
. 2
⊢ (((𝐴 ∪ 𝐵) ≼ ((𝐴 × {1o}) ∪ (𝐴 × {∅})) ∧
((𝐴 ×
{1o}) ∪ (𝐴
× {∅})) ≼ (𝐴 × 𝐴)) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |
33 | 21, 31, 32 | syl2anc 587 |
1
⊢
((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |