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 e. V /\ B e. W ) -> ( A |_| B ) e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prex | |- { (/) , 1o } e. _V |
|
| 2 | unexg | |- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V ) |
|
| 3 | xpexg | |- ( ( { (/) , 1o } e. _V /\ ( A u. B ) e. _V ) -> ( { (/) , 1o } X. ( A u. B ) ) e. _V ) |
|
| 4 | 1 2 3 | sylancr | |- ( ( A e. V /\ B e. W ) -> ( { (/) , 1o } X. ( A u. B ) ) e. _V ) |
| 5 | djuss | |- ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) ) |
|
| 6 | 5 | a1i | |- ( ( A e. V /\ B e. W ) -> ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) ) ) |
| 7 | 4 6 | ssexd | |- ( ( A e. V /\ B e. W ) -> ( A |_| B ) e. _V ) |