Theorem unxpdom

Description: Cartesian product dominates union for sets with cardinality greater than 1. Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 13-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex2i	⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
3	1	brrelex2i	⊢ ( 1o ≺ 𝐵 → 𝐵 ∈ V )
4	2 3	anim12i	⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5		breq2	⊢ ( 𝑥 = 𝐴 → ( 1o ≺ 𝑥 ↔ 1o ≺ 𝐴 ) )
6	5	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 1o ≺ 𝑥 ∧ 1o ≺ 𝑦 ) ↔ ( 1o ≺ 𝐴 ∧ 1o ≺ 𝑦 ) ) )
7		uneq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∪ 𝑦 ) = ( 𝐴 ∪ 𝑦 ) )
8		xpeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 × 𝑦 ) = ( 𝐴 × 𝑦 ) )
9	7 8	breq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∪ 𝑦 ) ≼ ( 𝑥 × 𝑦 ) ↔ ( 𝐴 ∪ 𝑦 ) ≼ ( 𝐴 × 𝑦 ) ) )
10	6 9	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 1o ≺ 𝑥 ∧ 1o ≺ 𝑦 ) → ( 𝑥 ∪ 𝑦 ) ≼ ( 𝑥 × 𝑦 ) ) ↔ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝑦 ) → ( 𝐴 ∪ 𝑦 ) ≼ ( 𝐴 × 𝑦 ) ) ) )
11		breq2	⊢ ( 𝑦 = 𝐵 → ( 1o ≺ 𝑦 ↔ 1o ≺ 𝐵 ) )
12	11	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝑦 ) ↔ ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) ) )
13		uneq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∪ 𝑦 ) = ( 𝐴 ∪ 𝐵 ) )
14		xpeq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 × 𝑦 ) = ( 𝐴 × 𝐵 ) )
15	13 14	breq12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∪ 𝑦 ) ≼ ( 𝐴 × 𝑦 ) ↔ ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) ) )
16	12 15	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝑦 ) → ( 𝐴 ∪ 𝑦 ) ≼ ( 𝐴 × 𝑦 ) ) ↔ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) ) ) )
17		eqid	⊢ ( 𝑧 ∈ ( 𝑥 ∪ 𝑦 ) ↦ if ( 𝑧 ∈ 𝑥 , ⟨ 𝑧 , if ( 𝑧 = 𝑣 , 𝑤 , 𝑡 ) ⟩ , ⟨ if ( 𝑧 = 𝑤 , 𝑢 , 𝑣 ) , 𝑧 ⟩ ) ) = ( 𝑧 ∈ ( 𝑥 ∪ 𝑦 ) ↦ if ( 𝑧 ∈ 𝑥 , ⟨ 𝑧 , if ( 𝑧 = 𝑣 , 𝑤 , 𝑡 ) ⟩ , ⟨ if ( 𝑧 = 𝑤 , 𝑢 , 𝑣 ) , 𝑧 ⟩ ) )
18		eqid	⊢ if ( 𝑧 ∈ 𝑥 , ⟨ 𝑧 , if ( 𝑧 = 𝑣 , 𝑤 , 𝑡 ) ⟩ , ⟨ if ( 𝑧 = 𝑤 , 𝑢 , 𝑣 ) , 𝑧 ⟩ ) = if ( 𝑧 ∈ 𝑥 , ⟨ 𝑧 , if ( 𝑧 = 𝑣 , 𝑤 , 𝑡 ) ⟩ , ⟨ if ( 𝑧 = 𝑤 , 𝑢 , 𝑣 ) , 𝑧 ⟩ )
19	17 18	unxpdomlem3	⊢ ( ( 1o ≺ 𝑥 ∧ 1o ≺ 𝑦 ) → ( 𝑥 ∪ 𝑦 ) ≼ ( 𝑥 × 𝑦 ) )
20	10 16 19	vtocl2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) ) )
21	4 20	mpcom	⊢ ( ( 1o ≺ 𝐴 ∧ 1o ≺ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )