Theorem undjudom

Description: Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004) (Revised by Jim Kingdon, 15-Aug-2023)

	Ref	Expression
Assertion	undjudom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
3	1 2	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
4		ensym	⊢ ( ( { ∅ } × 𝐴 ) ≈ 𝐴 → 𝐴 ≈ ( { ∅ } × 𝐴 ) )
5		endom	⊢ ( 𝐴 ≈ ( { ∅ } × 𝐴 ) → 𝐴 ≼ ( { ∅ } × 𝐴 ) )
6	3 4 5	3syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ ( { ∅ } × 𝐴 ) )
7		1on	⊢ 1o ∈ On
8		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐵 ∈ 𝑊 ) → ( { 1o } × 𝐵 ) ≈ 𝐵 )
9	7 8	mpan	⊢ ( 𝐵 ∈ 𝑊 → ( { 1o } × 𝐵 ) ≈ 𝐵 )
10		ensym	⊢ ( ( { 1o } × 𝐵 ) ≈ 𝐵 → 𝐵 ≈ ( { 1o } × 𝐵 ) )
11		endom	⊢ ( 𝐵 ≈ ( { 1o } × 𝐵 ) → 𝐵 ≼ ( { 1o } × 𝐵 ) )
12	9 10 11	3syl	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ≼ ( { 1o } × 𝐵 ) )
13		xp01disjl	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅
14		undom	⊢ ( ( ( 𝐴 ≼ ( { ∅ } × 𝐴 ) ∧ 𝐵 ≼ ( { 1o } × 𝐵 ) ) ∧ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐵 ) ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
15	13 14	mpan2	⊢ ( ( 𝐴 ≼ ( { ∅ } × 𝐴 ) ∧ 𝐵 ≼ ( { 1o } × 𝐵 ) ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
16	6 12 15	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
17		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
18	16 17	breqtrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )