Proof of Theorem unxpdom2
Step | Hyp | Ref
| Expression |
1 | | relsdom 7962 |
. . . . . . . 8
⊢ Rel
≺ |
2 | 1 | brrelex2i 5159 |
. . . . . . 7
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ V) |
3 | 2 | adantr 481 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V) |
4 | | 1onn 7719 |
. . . . . 6
⊢
1𝑜 ∈ ω |
5 | | xpsneng 8045 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ ω) → (𝐴 × {1𝑜}) ≈
𝐴) |
6 | 3, 4, 5 | sylancl 694 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {1𝑜}) ≈
𝐴) |
7 | 6 | ensymd 8007 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 ×
{1𝑜})) |
8 | | endom 7982 |
. . . 4
⊢ (𝐴 ≈ (𝐴 × {1𝑜}) →
𝐴 ≼ (𝐴 ×
{1𝑜})) |
9 | 7, 8 | syl 17 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≼ (𝐴 ×
{1𝑜})) |
10 | | simpr 477 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ 𝐴) |
11 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
12 | | xpsneng 8045 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
13 | 3, 11, 12 | sylancl 694 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × {∅}) ≈ 𝐴) |
14 | 13 | ensymd 8007 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ (𝐴 × {∅})) |
15 | | domentr 8015 |
. . . 4
⊢ ((𝐵 ≼ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) → 𝐵 ≼ (𝐴 × {∅})) |
16 | 10, 14, 15 | syl2anc 693 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 𝐵 ≼ (𝐴 × {∅})) |
17 | | 1n0 7575 |
. . . 4
⊢
1𝑜 ≠ ∅ |
18 | | xpsndisj 5557 |
. . . 4
⊢
(1𝑜 ≠ ∅ → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
19 | 17, 18 | mp1i 13 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∩
(𝐴 × {∅})) =
∅) |
20 | | undom 8048 |
. . 3
⊢ (((𝐴 ≼ (𝐴 × {1𝑜}) ∧
𝐵 ≼ (𝐴 × {∅})) ∧
((𝐴 ×
{1𝑜}) ∩ (𝐴 × {∅})) = ∅) →
(𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
21 | 9, 16, 19, 20 | syl21anc 1325 |
. 2
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 ×
{∅}))) |
22 | | sdomentr 8094 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {1𝑜})) →
1𝑜 ≺ (𝐴 ×
{1𝑜})) |
23 | 7, 22 | syldan 487 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1𝑜 ≺
(𝐴 ×
{1𝑜})) |
24 | | sdomentr 8094 |
. . . . 5
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐴 ≈ (𝐴 × {∅})) →
1𝑜 ≺ (𝐴 × {∅})) |
25 | 14, 24 | syldan 487 |
. . . 4
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → 1𝑜 ≺
(𝐴 ×
{∅})) |
26 | | unxpdom 8167 |
. . . 4
⊢
((1𝑜 ≺ (𝐴 × {1𝑜}) ∧
1𝑜 ≺ (𝐴 × {∅})) → ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
27 | 23, 25, 26 | syl2anc 693 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅}))) |
28 | | xpen 8123 |
. . . 4
⊢ (((𝐴 ×
{1𝑜}) ≈ 𝐴 ∧ (𝐴 × {∅}) ≈ 𝐴) → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
29 | 6, 13, 28 | syl2anc 693 |
. . 3
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ×
(𝐴 × {∅}))
≈ (𝐴 × 𝐴)) |
30 | | domentr 8015 |
. . 3
⊢ ((((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅})) ∧ ((𝐴 ×
{1𝑜}) × (𝐴 × {∅})) ≈ (𝐴 × 𝐴)) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ (𝐴 × 𝐴)) |
31 | 27, 29, 30 | syl2anc 693 |
. 2
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
≼ (𝐴 × 𝐴)) |
32 | | domtr 8009 |
. 2
⊢ (((𝐴 ∪ 𝐵) ≼ ((𝐴 × {1𝑜}) ∪
(𝐴 × {∅}))
∧ ((𝐴 ×
{1𝑜}) ∪ (𝐴 × {∅})) ≼ (𝐴 × 𝐴)) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |
33 | 21, 31, 32 | syl2anc 693 |
1
⊢
((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) |