Metamath Proof Explorer

Theorem djuexALT

Description: Alternate proof of djuex , which is shorter, but based indirectly on the definitions of inl and inr . (Proposed by BJ, 28-Jun-2022.) (Contributed by AV, 28-Jun-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion djuexALT ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ∈ V

Proof

Step Hyp Ref Expression
1 prex ⊢ ∅ 1 𝑜 ∈ V
2 unexg ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V
3 xpexg ⊢ ∅ 1 𝑜 ∈ V ∧ A ∪ B ∈ V → ∅ 1 𝑜 × A ∪ B ∈ V
4 1 2 3 sylancr ⊢ A ∈ V ∧ B ∈ W → ∅ 1 𝑜 × A ∪ B ∈ V
5 djuss ⊢ A ⊔︀ B ⊆ ∅ 1 𝑜 × A ∪ B
6 5 a1i ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ⊆ ∅ 1 𝑜 × A ∪ B
7 4 6 ssexd ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ∈ V