Step |
Hyp |
Ref |
Expression |
1 |
|
ctex |
⊢ ( 𝐵 ≼ ω → 𝐵 ∈ V ) |
2 |
1
|
adantl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐵 ∈ V ) |
3 |
|
simpl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → 𝐴 ≼ ω ) |
4 |
|
xpdom1g |
⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) ) |
5 |
2 3 4
|
syl2anc |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) ) |
6 |
|
omex |
⊢ ω ∈ V |
7 |
6
|
xpdom2 |
⊢ ( 𝐵 ≼ ω → ( ω × 𝐵 ) ≼ ( ω × ω ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( ω × 𝐵 ) ≼ ( ω × ω ) ) |
9 |
|
domtr |
⊢ ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × 𝐵 ) ∧ ( ω × 𝐵 ) ≼ ( ω × ω ) ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) ) |
10 |
5 8 9
|
syl2anc |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) ) |
11 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
12 |
|
domentr |
⊢ ( ( ( 𝐴 × 𝐵 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝐴 × 𝐵 ) ≼ ω ) |
13 |
10 11 12
|
sylancl |
⊢ ( ( 𝐴 ≼ ω ∧ 𝐵 ≼ ω ) → ( 𝐴 × 𝐵 ) ≼ ω ) |