Theorem djudoml

Description: A set is dominated by its disjoint union with another. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
2		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
3		ssdomg	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ) )
4	1 2 3	mpisyl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) )
5		undjudom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
6		domtr	⊢ ( ( 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
7	4 5 6	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )