This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djuxpdom

Description: Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion djuxpdom ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
2 0ex ⊢ ∅ ∈ V
3 relsdom ⊢ Rel ≺
4 3 brrelex2i ⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
5 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
6 2 4 5 sylancr ⊢ ( 1o ≺ 𝐴 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
7 sdomen2 ⊢ ( ( { ∅ } × 𝐴 ) ≈ 𝐴 → ( 1o ≺ ( { ∅ } × 𝐴 ) ↔ 1o ≺ 𝐴 ) )
8 6 7 syl ⊢ ( 1o ≺ 𝐴 → ( 1o ≺ ( { ∅ } × 𝐴 ) ↔ 1o ≺ 𝐴 ) )
9 8 ibir ⊢ ( 1o ≺ 𝐴 → 1o ≺ ( { ∅ } × 𝐴 ) )
10 1on ⊢ 1o ∈ On
11 3 brrelex2i ⊢ ( 1o ≺ 𝐵 → 𝐵 ∈ V )
12 xpsnen2g ⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ V ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
13 10 11 12 sylancr ⊢ ( 1o ≺ 𝐵 → ( { 1o } × 𝐵 ) ≈ 𝐵 )
14 sdomen2 ⊢ ( ( { 1o } × 𝐵 ) ≈ 𝐵 → ( 1o ≺ ( { 1o } × 𝐵 ) ↔ 1o ≺ 𝐵 ) )
15 13 14 syl ⊢ ( 1o ≺ 𝐵 → ( 1o ≺ ( { 1o } × 𝐵 ) ↔ 1o ≺ 𝐵 ) )
16 15 ibir ⊢ ( 1o ≺ 𝐵 → 1o ≺ ( { 1o } × 𝐵 ) )
17 unxpdom ⊢ ( ( 1o ≺ ( { ∅ } × 𝐴 ) ∧ 1o ≺ ( { 1o } × 𝐵 ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≼ ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) )
18 9 16 17 syl2an ⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ≼ ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) )
19 1 18 eqbrtrid ⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) )
20 xpen ⊢ ( ( ( { ∅ } × 𝐴 ) ≈ 𝐴 ∧ ( { 1o } × 𝐵 ) ≈ 𝐵 ) → ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 × 𝐵 ) )
21 6 13 20 syl2an ⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 × 𝐵 ) )
22 domentr ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) ∧ ( ( { ∅ } × 𝐴 ) × ( { 1o } × 𝐵 ) ) ≈ ( 𝐴 × 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
23 19 21 22 syl2anc ⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )