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 ⊢ A ∈ V ∧ B ∈ W → A ∪ B ≼ A ⊔︀ B

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 xpsnen2g ⊢ ∅ ∈ V ∧ A ∈ V → ∅ × A ≈ A
3 1 2 mpan ⊢ A ∈ V → ∅ × A ≈ A
4 ensym ⊢ ∅ × A ≈ A → A ≈ ∅ × A
5 endom ⊢ A ≈ ∅ × A → A ≼ ∅ × A
6 3 4 5 3syl ⊢ A ∈ V → A ≼ ∅ × A
7 1on ⊢ 1 𝑜 ∈ On
8 xpsnen2g ⊢ 1 𝑜 ∈ On ∧ B ∈ W → 1 𝑜 × B ≈ B
9 7 8 mpan ⊢ B ∈ W → 1 𝑜 × B ≈ B
10 ensym ⊢ 1 𝑜 × B ≈ B → B ≈ 1 𝑜 × B
11 endom ⊢ B ≈ 1 𝑜 × B → B ≼ 1 𝑜 × B
12 9 10 11 3syl ⊢ B ∈ W → B ≼ 1 𝑜 × B
13 xp01disjl ⊢ ∅ × A ∩ 1 𝑜 × B = ∅
14 undom ⊢ A ≼ ∅ × A ∧ B ≼ 1 𝑜 × B ∧ ∅ × A ∩ 1 𝑜 × B = ∅ → A ∪ B ≼ ∅ × A ∪ 1 𝑜 × B
15 13 14 mpan2 ⊢ A ≼ ∅ × A ∧ B ≼ 1 𝑜 × B → A ∪ B ≼ ∅ × A ∪ 1 𝑜 × B
16 6 12 15 syl2an ⊢ A ∈ V ∧ B ∈ W → A ∪ B ≼ ∅ × A ∪ 1 𝑜 × B
17 df-dju ⊢ A ⊔︀ B = ∅ × A ∪ 1 𝑜 × B
18 16 17 breqtrrdi ⊢ A ∈ V ∧ B ∈ W → A ∪ B ≼ A ⊔︀ B