This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unxpdom2

Description: Corollary of unxpdom . (Contributed by NM, 16-Sep-2004)

Ref Expression
Assertion unxpdom2 
|- ( ( 1o ~< A /\ B ~<_ A ) -> ( A u. B ) ~<_ ( A X. A ) )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex2i 
 |-  ( 1o ~< A -> A e. _V )
3 2 adantr 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> A e. _V )
4 1onn 
 |-  1o e. _om
5 xpsneng 
 |-  ( ( A e. _V /\ 1o e. _om ) -> ( A X. { 1o } ) ~~ A )
6 3 4 5 sylancl 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( A X. { 1o } ) ~~ A )
7 6 ensymd 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> A ~~ ( A X. { 1o } ) )
8 endom 
 |-  ( A ~~ ( A X. { 1o } ) -> A ~<_ ( A X. { 1o } ) )
9 7 8 syl 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> A ~<_ ( A X. { 1o } ) )
10 simpr 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> B ~<_ A )
11 0ex 
 |-  (/) e. _V
12 xpsneng 
 |-  ( ( A e. _V /\ (/) e. _V ) -> ( A X. { (/) } ) ~~ A )
13 3 11 12 sylancl 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( A X. { (/) } ) ~~ A )
14 13 ensymd 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> A ~~ ( A X. { (/) } ) )
15 domentr 
 |-  ( ( B ~<_ A /\ A ~~ ( A X. { (/) } ) ) -> B ~<_ ( A X. { (/) } ) )
16 10 14 15 syl2anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> B ~<_ ( A X. { (/) } ) )
17 1n0 
 |-  1o =/= (/)
18 xpsndisj 
 |-  ( 1o =/= (/) -> ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) )
19 17 18 mp1i 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) )
20 undom 
 |-  ( ( ( A ~<_ ( A X. { 1o } ) /\ B ~<_ ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) i^i ( A X. { (/) } ) ) = (/) ) -> ( A u. B ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) )
21 9 16 19 20 syl21anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( A u. B ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) )
22 sdomentr 
 |-  ( ( 1o ~< A /\ A ~~ ( A X. { 1o } ) ) -> 1o ~< ( A X. { 1o } ) )
23 7 22 syldan 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> 1o ~< ( A X. { 1o } ) )
24 sdomentr 
 |-  ( ( 1o ~< A /\ A ~~ ( A X. { (/) } ) ) -> 1o ~< ( A X. { (/) } ) )
25 14 24 syldan 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> 1o ~< ( A X. { (/) } ) )
26 unxpdom 
 |-  ( ( 1o ~< ( A X. { 1o } ) /\ 1o ~< ( A X. { (/) } ) ) -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
27 23 25 26 syl2anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) )
28 xpen 
 |-  ( ( ( A X. { 1o } ) ~~ A /\ ( A X. { (/) } ) ~~ A ) -> ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) )
29 6 13 28 syl2anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) )
30 domentr 
 |-  ( ( ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) X. ( A X. { (/) } ) ) ~~ ( A X. A ) ) -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( A X. A ) )
31 27 29 30 syl2anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( A X. A ) )
32 domtr 
 |-  ( ( ( A u. B ) ~<_ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) /\ ( ( A X. { 1o } ) u. ( A X. { (/) } ) ) ~<_ ( A X. A ) ) -> ( A u. B ) ~<_ ( A X. A ) )
33 21 31 32 syl2anc 
 |-  ( ( 1o ~< A /\ B ~<_ A ) -> ( A u. B ) ~<_ ( A X. A ) )