Step |
Hyp |
Ref |
Expression |
1 |
|
ctex |
⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V ) |
2 |
|
ctex |
⊢ ( 𝐵 ≼ ω → 𝐵 ∈ V ) |
3 |
|
undjudom |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) |
5 |
|
djudom1 |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ∈ V ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ 𝐵 ) ) |
6 |
2 5
|
sylan2 |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ 𝐵 ) ) |
7 |
|
simpr |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐵 ≼ ω ) |
8 |
|
omex |
⊢ ω ∈ V |
9 |
|
djudom2 |
⊢ ( ( 𝐵 ≼ ω ∧ ω ∈ V ) → ( ω ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ) |
10 |
7 8 9
|
sylancl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( ω ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ) |
11 |
|
domtr |
⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ 𝐵 ) ∧ ( ω ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ) |
12 |
6 10 11
|
syl2anc |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ) |
13 |
8 8
|
xpex |
⊢ ( ω × ω ) ∈ V |
14 |
|
xp2dju |
⊢ ( 2o × ω ) = ( ω ⊔ ω ) |
15 |
|
ordom |
⊢ Ord ω |
16 |
|
2onn |
⊢ 2o ∈ ω |
17 |
|
ordelss |
⊢ ( ( Ord ω ∧ 2o ∈ ω ) → 2o ⊆ ω ) |
18 |
15 16 17
|
mp2an |
⊢ 2o ⊆ ω |
19 |
|
xpss1 |
⊢ ( 2o ⊆ ω → ( 2o × ω ) ⊆ ( ω × ω ) ) |
20 |
18 19
|
ax-mp |
⊢ ( 2o × ω ) ⊆ ( ω × ω ) |
21 |
14 20
|
eqsstrri |
⊢ ( ω ⊔ ω ) ⊆ ( ω × ω ) |
22 |
|
ssdomg |
⊢ ( ( ω × ω ) ∈ V → ( ( ω ⊔ ω ) ⊆ ( ω × ω ) → ( ω ⊔ ω ) ≼ ( ω × ω ) ) ) |
23 |
13 21 22
|
mp2 |
⊢ ( ω ⊔ ω ) ≼ ( ω × ω ) |
24 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
25 |
|
domentr |
⊢ ( ( ( ω ⊔ ω ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( ω ⊔ ω ) ≼ ω ) |
26 |
23 24 25
|
mp2an |
⊢ ( ω ⊔ ω ) ≼ ω |
27 |
|
domtr |
⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( ω ⊔ ω ) ∧ ( ω ⊔ ω ) ≼ ω ) → ( 𝐴 ⊔ 𝐵 ) ≼ ω ) |
28 |
12 26 27
|
sylancl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 ⊔ 𝐵 ) ≼ ω ) |
29 |
|
domtr |
⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≼ ω ) → ( 𝐴 ∪ 𝐵 ) ≼ ω ) |
30 |
4 28 29
|
syl2anc |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 ∪ 𝐵 ) ≼ ω ) |