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𝐵 ) → ( 𝐴𝐵 ) ≼ ( 𝐴 × 𝐵 ) )