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