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 ) )