Metamath Proof Explorer

Theorem unxpwdom2

Description: Lemma for unxpwdom . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion unxpwdom2 
|- ( ( A X. A ) ~~ ( B u. C ) -> ( A ~<_* B \/ A ~<_ C ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( ( A X. A ) ~~ ( B u. C ) -> ( B u. C ) ~~ ( A X. A ) )
2 bren 
 |-  ( ( B u. C ) ~~ ( A X. A ) <-> E. f f : ( B u. C ) -1-1-onto-> ( A X. A ) )
3 ssdif0 
 |-  ( A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) <-> ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) = (/) )
4 dmxpid 
 |-  dom ( A X. A ) = A
5 f1ofo 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> f : ( B u. C ) -onto-> ( A X. A ) )
6 forn 
 |-  ( f : ( B u. C ) -onto-> ( A X. A ) -> ran f = ( A X. A ) )
7 5 6 syl 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ran f = ( A X. A ) )
8 vex 
 |-  f e. _V
9 8 rnex 
 |-  ran f e. _V
10 7 9 eqeltrrdi 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( A X. A ) e. _V )
11 10 dmexd 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> dom ( A X. A ) e. _V )
12 4 11 eqeltrrid 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> A e. _V )
13 imassrn 
 |-  ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) C_ ran ( ( 1st |` ( A X. A ) ) o. f )
14 f1stres 
 |-  ( 1st |` ( A X. A ) ) : ( A X. A ) --> A
15 f1of 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> f : ( B u. C ) --> ( A X. A ) )
16 fco 
 |-  ( ( ( 1st |` ( A X. A ) ) : ( A X. A ) --> A /\ f : ( B u. C ) --> ( A X. A ) ) -> ( ( 1st |` ( A X. A ) ) o. f ) : ( B u. C ) --> A )
17 14 15 16 sylancr 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( 1st |` ( A X. A ) ) o. f ) : ( B u. C ) --> A )
18 17 frnd 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ran ( ( 1st |` ( A X. A ) ) o. f ) C_ A )
19 13 18 sstrid 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) C_ A )
20 12 19 ssexd 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) e. _V )
21 20 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) e. _V )
22 simpr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
23 ssdomg 
 |-  ( ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) e. _V -> ( A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) -> A ~<_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) )
24 21 22 23 sylc 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> A ~<_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
25 domwdom 
 |-  ( A ~<_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) -> A ~<_* ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
26 24 25 syl 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> A ~<_* ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
27 17 ffund 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> Fun ( ( 1st |` ( A X. A ) ) o. f ) )
28 ssun1 
 |-  B C_ ( B u. C )
29 f1odm 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> dom f = ( B u. C ) )
30 8 dmex 
 |-  dom f e. _V
31 29 30 eqeltrrdi 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( B u. C ) e. _V )
32 ssexg 
 |-  ( ( B C_ ( B u. C ) /\ ( B u. C ) e. _V ) -> B e. _V )
33 28 31 32 sylancr 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> B e. _V )
34 wdomima2g 
 |-  ( ( Fun ( ( 1st |` ( A X. A ) ) o. f ) /\ B e. _V /\ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) e. _V ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ~<_* B )
35 27 33 20 34 syl3anc 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ~<_* B )
36 35 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ~<_* B )
37 wdomtr 
 |-  ( ( A ~<_* ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) /\ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ~<_* B ) -> A ~<_* B )
38 26 36 37 syl2anc 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> A ~<_* B )
39 38 orcd 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> ( A ~<_* B \/ A ~<_ C ) )
40 39 ex 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( A C_ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) -> ( A ~<_* B \/ A ~<_ C ) ) )
41 3 40 syl5bir 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) = (/) -> ( A ~<_* B \/ A ~<_ C ) ) )
42 n0 
 |-  ( ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) =/= (/) <-> E. x x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) )
43 ssun2 
 |-  C C_ ( B u. C )
44 ssexg 
 |-  ( ( C C_ ( B u. C ) /\ ( B u. C ) e. _V ) -> C e. _V )
45 43 31 44 sylancr 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> C e. _V )
46 45 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> C e. _V )
47 f1ofn 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> f Fn ( B u. C ) )
48 elpreima 
 |-  ( f Fn ( B u. C ) -> ( y e. ( `' f " ( { x } X. A ) ) <-> ( y e. ( B u. C ) /\ ( f ` y ) e. ( { x } X. A ) ) ) )
49 47 48 syl 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( y e. ( `' f " ( { x } X. A ) ) <-> ( y e. ( B u. C ) /\ ( f ` y ) e. ( { x } X. A ) ) ) )
50 49 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( y e. ( `' f " ( { x } X. A ) ) <-> ( y e. ( B u. C ) /\ ( f ` y ) e. ( { x } X. A ) ) ) )
51 elun 
 |-  ( y e. ( B u. C ) <-> ( y e. B \/ y e. C ) )
52 df-or 
 |-  ( ( y e. B \/ y e. C ) <-> ( -. y e. B -> y e. C ) )
53 51 52 bitri 
 |-  ( y e. ( B u. C ) <-> ( -. y e. B -> y e. C ) )
54 eldifn 
 |-  ( x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> -. x e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
55 54 ad2antlr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( f ` y ) e. ( { x } X. A ) ) -> -. x e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
56 15 ad2antrr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> f : ( B u. C ) --> ( A X. A ) )
57 simprr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> y e. B )
58 28 57 sselid 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> y e. ( B u. C ) )
59 fvco3 
 |-  ( ( f : ( B u. C ) --> ( A X. A ) /\ y e. ( B u. C ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) ` y ) = ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) )
60 56 58 59 syl2anc 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) ` y ) = ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) )
61 eldifi 
 |-  ( x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> x e. A )
62 61 adantl 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> x e. A )
63 62 snssd 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> { x } C_ A )
64 xpss1 
 |-  ( { x } C_ A -> ( { x } X. A ) C_ ( A X. A ) )
65 63 64 syl 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( { x } X. A ) C_ ( A X. A ) )
66 65 adantr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( { x } X. A ) C_ ( A X. A ) )
67 simprl 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( f ` y ) e. ( { x } X. A ) )
68 66 67 sseldd 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( f ` y ) e. ( A X. A ) )
69 68 fvresd 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) = ( 1st ` ( f ` y ) ) )
70 xp1st 
 |-  ( ( f ` y ) e. ( { x } X. A ) -> ( 1st ` ( f ` y ) ) e. { x } )
71 67 70 syl 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( 1st ` ( f ` y ) ) e. { x } )
72 69 71 eqeltrd 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) e. { x } )
73 elsni 
 |-  ( ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) e. { x } -> ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) = x )
74 72 73 syl 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( 1st |` ( A X. A ) ) ` ( f ` y ) ) = x )
75 60 74 eqtrd 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) ` y ) = x )
76 17 ffnd 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( 1st |` ( A X. A ) ) o. f ) Fn ( B u. C ) )
77 76 ad2antrr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( 1st |` ( A X. A ) ) o. f ) Fn ( B u. C ) )
78 28 a1i 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> B C_ ( B u. C ) )
79 fnfvima 
 |-  ( ( ( ( 1st |` ( A X. A ) ) o. f ) Fn ( B u. C ) /\ B C_ ( B u. C ) /\ y e. B ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) ` y ) e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
80 77 78 57 79 syl3anc 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> ( ( ( 1st |` ( A X. A ) ) o. f ) ` y ) e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
81 75 80 eqeltrrd 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( ( f ` y ) e. ( { x } X. A ) /\ y e. B ) ) -> x e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) )
82 81 expr 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( f ` y ) e. ( { x } X. A ) ) -> ( y e. B -> x e. ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) )
83 55 82 mtod 
 |-  ( ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) /\ ( f ` y ) e. ( { x } X. A ) ) -> -. y e. B )
84 83 ex 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( ( f ` y ) e. ( { x } X. A ) -> -. y e. B ) )
85 84 imim1d 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( ( -. y e. B -> y e. C ) -> ( ( f ` y ) e. ( { x } X. A ) -> y e. C ) ) )
86 53 85 syl5bi 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( y e. ( B u. C ) -> ( ( f ` y ) e. ( { x } X. A ) -> y e. C ) ) )
87 86 impd 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( ( y e. ( B u. C ) /\ ( f ` y ) e. ( { x } X. A ) ) -> y e. C ) )
88 50 87 sylbid 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( y e. ( `' f " ( { x } X. A ) ) -> y e. C ) )
89 88 ssrdv 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( `' f " ( { x } X. A ) ) C_ C )
90 ssdomg 
 |-  ( C e. _V -> ( ( `' f " ( { x } X. A ) ) C_ C -> ( `' f " ( { x } X. A ) ) ~<_ C ) )
91 46 89 90 sylc 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( `' f " ( { x } X. A ) ) ~<_ C )
92 f1ocnv 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> `' f : ( A X. A ) -1-1-onto-> ( B u. C ) )
93 f1of1 
 |-  ( `' f : ( A X. A ) -1-1-onto-> ( B u. C ) -> `' f : ( A X. A ) -1-1-> ( B u. C ) )
94 92 93 syl 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> `' f : ( A X. A ) -1-1-> ( B u. C ) )
95 94 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> `' f : ( A X. A ) -1-1-> ( B u. C ) )
96 31 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( B u. C ) e. _V )
97 snex 
 |-  { x } e. _V
98 12 adantr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> A e. _V )
99 xpexg 
 |-  ( ( { x } e. _V /\ A e. _V ) -> ( { x } X. A ) e. _V )
100 97 98 99 sylancr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( { x } X. A ) e. _V )
101 f1imaen2g 
 |-  ( ( ( `' f : ( A X. A ) -1-1-> ( B u. C ) /\ ( B u. C ) e. _V ) /\ ( ( { x } X. A ) C_ ( A X. A ) /\ ( { x } X. A ) e. _V ) ) -> ( `' f " ( { x } X. A ) ) ~~ ( { x } X. A ) )
102 95 96 65 100 101 syl22anc 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( `' f " ( { x } X. A ) ) ~~ ( { x } X. A ) )
103 vex 
 |-  x e. _V
104 xpsnen2g 
 |-  ( ( x e. _V /\ A e. _V ) -> ( { x } X. A ) ~~ A )
105 103 98 104 sylancr 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( { x } X. A ) ~~ A )
106 entr 
 |-  ( ( ( `' f " ( { x } X. A ) ) ~~ ( { x } X. A ) /\ ( { x } X. A ) ~~ A ) -> ( `' f " ( { x } X. A ) ) ~~ A )
107 102 105 106 syl2anc 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( `' f " ( { x } X. A ) ) ~~ A )
108 domen1 
 |-  ( ( `' f " ( { x } X. A ) ) ~~ A -> ( ( `' f " ( { x } X. A ) ) ~<_ C <-> A ~<_ C ) )
109 107 108 syl 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( ( `' f " ( { x } X. A ) ) ~<_ C <-> A ~<_ C ) )
110 91 109 mpbid 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> A ~<_ C )
111 110 olcd 
 |-  ( ( f : ( B u. C ) -1-1-onto-> ( A X. A ) /\ x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) ) -> ( A ~<_* B \/ A ~<_ C ) )
112 111 ex 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> ( A ~<_* B \/ A ~<_ C ) ) )
113 112 exlimdv 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( E. x x e. ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) -> ( A ~<_* B \/ A ~<_ C ) ) )
114 42 113 syl5bi 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( ( A \ ( ( ( 1st |` ( A X. A ) ) o. f ) " B ) ) =/= (/) -> ( A ~<_* B \/ A ~<_ C ) ) )
115 41 114 pm2.61dne 
 |-  ( f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( A ~<_* B \/ A ~<_ C ) )
116 115 exlimiv 
 |-  ( E. f f : ( B u. C ) -1-1-onto-> ( A X. A ) -> ( A ~<_* B \/ A ~<_ C ) )
117 2 116 sylbi 
 |-  ( ( B u. C ) ~~ ( A X. A ) -> ( A ~<_* B \/ A ~<_ C ) )
118 1 117 syl 
 |-  ( ( A X. A ) ~~ ( B u. C ) -> ( A ~<_* B \/ A ~<_ C ) )