Metamath Proof Explorer

Theorem iunconnlem

Description: Lemma for iunconn . (Contributed by Mario Carneiro, 11-Jun-2014)

Ref Expression
Hypotheses iunconn.2 
|- ( ph -> J e. ( TopOn ` X ) )
iunconn.3 
|- ( ( ph /\ k e. A ) -> B C_ X )
iunconn.4 
|- ( ( ph /\ k e. A ) -> P e. B )
iunconn.5 
|- ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
iunconn.6 
|- ( ph -> U e. J )
iunconn.7 
|- ( ph -> V e. J )
iunconn.8 
|- ( ph -> ( V i^i U_ k e. A B ) =/= (/) )
iunconn.9 
|- ( ph -> ( U i^i V ) C_ ( X \ U_ k e. A B ) )
iunconn.10 
|- ( ph -> U_ k e. A B C_ ( U u. V ) )
iunconn.11 
|- F/ k ph
Assertion iunconnlem 
|- ( ph -> -. P e. U )

Proof

Step Hyp Ref Expression
1 iunconn.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 iunconn.3 
 |-  ( ( ph /\ k e. A ) -> B C_ X )
3 iunconn.4 
 |-  ( ( ph /\ k e. A ) -> P e. B )
4 iunconn.5 
 |-  ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
5 iunconn.6 
 |-  ( ph -> U e. J )
6 iunconn.7 
 |-  ( ph -> V e. J )
7 iunconn.8 
 |-  ( ph -> ( V i^i U_ k e. A B ) =/= (/) )
8 iunconn.9 
 |-  ( ph -> ( U i^i V ) C_ ( X \ U_ k e. A B ) )
9 iunconn.10 
 |-  ( ph -> U_ k e. A B C_ ( U u. V ) )
10 iunconn.11 
 |-  F/ k ph
11 n0 
 |-  ( ( V i^i U_ k e. A B ) =/= (/) <-> E. x x e. ( V i^i U_ k e. A B ) )
12 7 11 sylib 
 |-  ( ph -> E. x x e. ( V i^i U_ k e. A B ) )
13 elin 
 |-  ( x e. ( V i^i U_ k e. A B ) <-> ( x e. V /\ x e. U_ k e. A B ) )
14 eliun 
 |-  ( x e. U_ k e. A B <-> E. k e. A x e. B )
15 nfv 
 |-  F/ k x e. V
16 10 15 nfan 
 |-  F/ k ( ph /\ x e. V )
17 nfv 
 |-  F/ k -. P e. U
18 4 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ ( x e. V /\ x e. B ) ) -> ( J |`t B ) e. Conn )
19 1 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> J e. ( TopOn ` X ) )
20 2 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> B C_ X )
21 5 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> U e. J )
22 6 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> V e. J )
23 simprr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> P e. U )
24 3 adantr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> P e. B )
25 inelcm 
 |-  ( ( P e. U /\ P e. B ) -> ( U i^i B ) =/= (/) )
26 23 24 25 syl2anc 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( U i^i B ) =/= (/) )
27 inelcm 
 |-  ( ( x e. V /\ x e. B ) -> ( V i^i B ) =/= (/) )
28 27 ad2antrl 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( V i^i B ) =/= (/) )
29 8 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( U i^i V ) C_ ( X \ U_ k e. A B ) )
30 ssiun2 
 |-  ( k e. A -> B C_ U_ k e. A B )
31 30 ad2antlr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> B C_ U_ k e. A B )
32 31 sscond 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( X \ U_ k e. A B ) C_ ( X \ B ) )
33 29 32 sstrd 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( U i^i V ) C_ ( X \ B ) )
34 inss1 
 |-  ( U i^i V ) C_ U
35 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U C_ X )
36 19 21 35 syl2anc 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> U C_ X )
37 34 36 sstrid 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( U i^i V ) C_ X )
38 reldisj 
 |-  ( ( U i^i V ) C_ X -> ( ( ( U i^i V ) i^i B ) = (/) <-> ( U i^i V ) C_ ( X \ B ) ) )
39 37 38 syl 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( ( ( U i^i V ) i^i B ) = (/) <-> ( U i^i V ) C_ ( X \ B ) ) )
40 33 39 mpbird 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> ( ( U i^i V ) i^i B ) = (/) )
41 9 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> U_ k e. A B C_ ( U u. V ) )
42 31 41 sstrd 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> B C_ ( U u. V ) )
43 19 20 21 22 26 28 40 42 nconnsubb 
 |-  ( ( ( ph /\ k e. A ) /\ ( ( x e. V /\ x e. B ) /\ P e. U ) ) -> -. ( J |`t B ) e. Conn )
44 43 expr 
 |-  ( ( ( ph /\ k e. A ) /\ ( x e. V /\ x e. B ) ) -> ( P e. U -> -. ( J |`t B ) e. Conn ) )
45 18 44 mt2d 
 |-  ( ( ( ph /\ k e. A ) /\ ( x e. V /\ x e. B ) ) -> -. P e. U )
46 45 an4s 
 |-  ( ( ( ph /\ x e. V ) /\ ( k e. A /\ x e. B ) ) -> -. P e. U )
47 46 exp32 
 |-  ( ( ph /\ x e. V ) -> ( k e. A -> ( x e. B -> -. P e. U ) ) )
48 16 17 47 rexlimd 
 |-  ( ( ph /\ x e. V ) -> ( E. k e. A x e. B -> -. P e. U ) )
49 14 48 syl5bi 
 |-  ( ( ph /\ x e. V ) -> ( x e. U_ k e. A B -> -. P e. U ) )
50 49 expimpd 
 |-  ( ph -> ( ( x e. V /\ x e. U_ k e. A B ) -> -. P e. U ) )
51 13 50 syl5bi 
 |-  ( ph -> ( x e. ( V i^i U_ k e. A B ) -> -. P e. U ) )
52 51 exlimdv 
 |-  ( ph -> ( E. x x e. ( V i^i U_ k e. A B ) -> -. P e. U ) )
53 12 52 mpd 
 |-  ( ph -> -. P e. U )