This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )