Proof of Theorem unxpdom2
Step | Hyp | Ref
| Expression |
1 | | relsdom 7848 |
. . . . . . . 8
⊢ Rel
≺ |
2 | 1 | brrelex2i 5083 |
. . . . . . 7
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ V) |
3 | 2 | adantr 480 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
4 | | 1onn 7606 |
. . . . . 6
⊢
1𝑜 ∈ ω |
5 | | xpsneng 7930 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ ω) → (𝐴 × {1𝑜}) ≈
𝐴) |
6 | 3, 4, 5 | sylancl 693 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {1𝑜}) ≈
𝐴) |
7 | 6 | ensymd 7893 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 ×
{1𝑜})) |
8 | | endom 7868 |
. . . 4
⊢ (𝐴 ≈ (𝐴 × {1𝑜}) →
𝐴 ≼ (𝐴 ×
{1𝑜})) |
9 | 7, 8 | syl 17 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≼ (𝐴 ×
{1𝑜})) |
10 | | simpr 476 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ 𝐴) |
11 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
12 | | xpsneng 7930 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
13 | 3, 11, 12 | sylancl 693 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {∅}) ≈ 𝐴) |
14 | 13 | ensymd 7893 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 × {∅})) |
15 | | domentr 7901 |
. . . 4
⊢ ((𝐵 ≼ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 𝐵 ≼ (𝐴 × {∅})) |
16 | 10, 14, 15 | syl2anc 691 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ (𝐴 × {∅})) |
17 | | 1n0 7462 |
. . . 4
⊢
1𝑜 ≠ ∅ |
18 | | xpsndisj 5476 |
. . . 4
⊢
(1𝑜 ≠ ∅ → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
19 | 17, 18 | mp1i 13 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
20 | | undom 7933 |
. . 3
⊢ (((𝐴 ≼ (𝐴 × {1𝑜}) ∧
𝐵 ≼ (𝐴 × {∅})) ∧
((𝐴 ×
{1𝑜}) ∩ (𝐴 × {∅})) = ∅) →
(𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
21 | 9, 16, 19, 20 | syl21anc 1317 |
. 2
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
22 | | sdomentr 7979 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1𝑜})) →
1𝑜 ≺ (𝐴 ×
{1𝑜})) |
23 | 7, 22 | syldan 486 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1𝑜 ≺
(𝐴 ×
{1𝑜})) |
24 | | sdomentr 7979 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) →
1𝑜 ≺ (𝐴 × {∅})) |
25 | 14, 24 | syldan 486 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1𝑜 ≺
(𝐴 ×
{∅})) |
26 | | unxpdom 8052 |
. . . 4
⊢
((1𝑜 ≺ (𝐴 × {1𝑜}) ∧
1𝑜 ≺ (𝐴 × {∅})) → ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
27 | 23, 25, 26 | syl2anc 691 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
28 | | xpen 8008 |
. . . 4
⊢ (((𝐴 ×
{1𝑜}) ≈ 𝐴 ∧ (𝐴 × {∅}) ≈ 𝐴) → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
29 | 6, 13, 28 | syl2anc 691 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
30 | | domentr 7901 |
. . 3
⊢ ((((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅})) ∧ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅})) ≈ (𝐴 × 𝐴)) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ (𝐴 × 𝐴)) |
31 | 27, 29, 30 | syl2anc 691 |
. 2
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ (𝐴 × 𝐴)) |
32 | | domtr 7895 |
. 2
⊢ (((𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
∧ ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ (𝐴 × 𝐴)) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |
33 | 21, 31, 32 | syl2anc 691 |
1
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |