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

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { ∅ , 1o } ∈ V
2		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
3		xpexg	⊢ ( ( { ∅ , 1o } ∈ V ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) ∈ V )
4	1 2 3	sylancr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) ∈ V )
5		djuss	⊢ ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) )
6	5	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
7	4 6	ssexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )