Metamath Proof Explorer

Theorem unxpdom2

Description: Corollary of unxpdom . (Contributed by NM, 16-Sep-2004)

Ref Expression
Assertion unxpdom2 ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 relsdom ⊢ Rel ≺
2 1 brrelex2i ⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
3 2 adantr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ∈ V )
4 1onn ⊢ 1o ∈ ω
5 xpsneng ⊢ ( ( 𝐴 ∈ V ∧ 1o ∈ ω ) → ( 𝐴 × { 1o } ) ≈ 𝐴 )
6 3 4 5 sylancl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 × { 1o } ) ≈ 𝐴 )
7 6 ensymd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ ( 𝐴 × { 1o } ) )
8 endom ⊢ ( 𝐴 ≈ ( 𝐴 × { 1o } ) → 𝐴 ≼ ( 𝐴 × { 1o } ) )
9 7 8 syl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≼ ( 𝐴 × { 1o } ) )
10 simpr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ≼ 𝐴 )
11 0ex ⊢ ∅ ∈ V
12 xpsneng ⊢ ( ( 𝐴 ∈ V ∧ ∅ ∈ V ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
13 3 11 12 sylancl ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
14 13 ensymd ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≈ ( 𝐴 × { ∅ } ) )
15 domentr ⊢ ( ( 𝐵 ≼ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { ∅ } ) ) → 𝐵 ≼ ( 𝐴 × { ∅ } ) )
16 10 14 15 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ≼ ( 𝐴 × { ∅ } ) )
17 1n0 ⊢ 1o ≠ ∅
18 xpsndisj ⊢ ( 1o ≠ ∅ → ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ )
19 17 18 mp1i ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ )
20 undom ⊢ ( ( ( 𝐴 ≼ ( 𝐴 × { 1o } ) ∧ 𝐵 ≼ ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) )
21 9 16 19 20 syl21anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) )
22 sdomentr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { 1o } ) ) → 1o ≺ ( 𝐴 × { 1o } ) )
23 7 22 syldan ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 1o ≺ ( 𝐴 × { 1o } ) )
24 sdomentr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { ∅ } ) ) → 1o ≺ ( 𝐴 × { ∅ } ) )
25 14 24 syldan ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 1o ≺ ( 𝐴 × { ∅ } ) )
26 unxpdom ⊢ ( ( 1o ≺ ( 𝐴 × { 1o } ) ∧ 1o ≺ ( 𝐴 × { ∅ } ) ) → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
27 23 25 26 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
28 xpen ⊢ ( ( ( 𝐴 × { 1o } ) ≈ 𝐴 ∧ ( 𝐴 × { ∅ } ) ≈ 𝐴 ) → ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) )
29 6 13 28 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) )
30 domentr ⊢ ( ( ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) ) → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( 𝐴 × 𝐴 ) )
31 27 29 30 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( 𝐴 × 𝐴 ) )
32 domtr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )
33 21 31 32 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )