Metamath Proof Explorer

Theorem unxpwdom

Description: If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

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

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( ( A X. A ) ~<_ ( B u. C ) -> ( B u. C ) e. _V )
3 domeng 
 |-  ( ( B u. C ) e. _V -> ( ( A X. A ) ~<_ ( B u. C ) <-> E. x ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) )
4 2 3 syl 
 |-  ( ( A X. A ) ~<_ ( B u. C ) -> ( ( A X. A ) ~<_ ( B u. C ) <-> E. x ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) )
5 4 ibi 
 |-  ( ( A X. A ) ~<_ ( B u. C ) -> E. x ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) )
6 simprl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A X. A ) ~~ x )
7 indi 
 |-  ( x i^i ( B u. C ) ) = ( ( x i^i B ) u. ( x i^i C ) )
8 simprr 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> x C_ ( B u. C ) )
9 df-ss 
 |-  ( x C_ ( B u. C ) <-> ( x i^i ( B u. C ) ) = x )
10 8 9 sylib 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( x i^i ( B u. C ) ) = x )
11 7 10 eqtr3id 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( ( x i^i B ) u. ( x i^i C ) ) = x )
12 6 11 breqtrrd 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A X. A ) ~~ ( ( x i^i B ) u. ( x i^i C ) ) )
13 unxpwdom2 
 |-  ( ( A X. A ) ~~ ( ( x i^i B ) u. ( x i^i C ) ) -> ( A ~<_* ( x i^i B ) \/ A ~<_ ( x i^i C ) ) )
14 12 13 syl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A ~<_* ( x i^i B ) \/ A ~<_ ( x i^i C ) ) )
15 ssun1 
 |-  B C_ ( B u. C )
16 2 adantr 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( B u. C ) e. _V )
17 ssexg 
 |-  ( ( B C_ ( B u. C ) /\ ( B u. C ) e. _V ) -> B e. _V )
18 15 16 17 sylancr 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> B e. _V )
19 inss2 
 |-  ( x i^i B ) C_ B
20 ssdomg 
 |-  ( B e. _V -> ( ( x i^i B ) C_ B -> ( x i^i B ) ~<_ B ) )
21 18 19 20 mpisyl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( x i^i B ) ~<_ B )
22 domwdom 
 |-  ( ( x i^i B ) ~<_ B -> ( x i^i B ) ~<_* B )
23 21 22 syl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( x i^i B ) ~<_* B )
24 wdomtr 
 |-  ( ( A ~<_* ( x i^i B ) /\ ( x i^i B ) ~<_* B ) -> A ~<_* B )
25 24 expcom 
 |-  ( ( x i^i B ) ~<_* B -> ( A ~<_* ( x i^i B ) -> A ~<_* B ) )
26 23 25 syl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A ~<_* ( x i^i B ) -> A ~<_* B ) )
27 ssun2 
 |-  C C_ ( B u. C )
28 ssexg 
 |-  ( ( C C_ ( B u. C ) /\ ( B u. C ) e. _V ) -> C e. _V )
29 27 16 28 sylancr 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> C e. _V )
30 inss2 
 |-  ( x i^i C ) C_ C
31 ssdomg 
 |-  ( C e. _V -> ( ( x i^i C ) C_ C -> ( x i^i C ) ~<_ C ) )
32 29 30 31 mpisyl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( x i^i C ) ~<_ C )
33 domtr 
 |-  ( ( A ~<_ ( x i^i C ) /\ ( x i^i C ) ~<_ C ) -> A ~<_ C )
34 33 expcom 
 |-  ( ( x i^i C ) ~<_ C -> ( A ~<_ ( x i^i C ) -> A ~<_ C ) )
35 32 34 syl 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A ~<_ ( x i^i C ) -> A ~<_ C ) )
36 26 35 orim12d 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( ( A ~<_* ( x i^i B ) \/ A ~<_ ( x i^i C ) ) -> ( A ~<_* B \/ A ~<_ C ) ) )
37 14 36 mpd 
 |-  ( ( ( A X. A ) ~<_ ( B u. C ) /\ ( ( A X. A ) ~~ x /\ x C_ ( B u. C ) ) ) -> ( A ~<_* B \/ A ~<_ C ) )
38 5 37 exlimddv 
 |-  ( ( A X. A ) ~<_ ( B u. C ) -> ( A ~<_* B \/ A ~<_ C ) )