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	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		prex	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}$$
2		unexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\cup B\in \mathrm{V}$$
3		xpexg	$$⊢\left(\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}\wedge A\cup B\in \mathrm{V}\right)\to \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\in \mathrm{V}$$
4	1 2 3	sylancr	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\in \mathrm{V}$$
5		djuss	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)\subseteq \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)$$
6	5	a1i	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\subseteq \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)$$
7	4 6	ssexd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\in \mathrm{V}$$