Metamath Proof Explorer

Theorem dfac14lem

Description: Lemma for dfac14 . By equipping S u. { P } for some P e/ S with the particular point topology, we can show that P is in the closure of S ; hence the sequence P ( x ) is in the product of the closures, and we can utilize this instance of ptcls to extract an element of the closure of X_ k e. I S . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses dfac14lem.i 
|- ( ph -> I e. V )
dfac14lem.s 
|- ( ( ph /\ x e. I ) -> S e. W )
dfac14lem.0 
|- ( ( ph /\ x e. I ) -> S =/= (/) )
dfac14lem.p 
|- P = ~P U. S
dfac14lem.r 
|- R = { y e. ~P ( S u. { P } ) | ( P e. y -> y = ( S u. { P } ) ) }
dfac14lem.j 
|- J = ( Xt_ ` ( x e. I |-> R ) )
dfac14lem.c 
|- ( ph -> ( ( cls ` J ) ` X_ x e. I S ) = X_ x e. I ( ( cls ` R ) ` S ) )
Assertion dfac14lem 
|- ( ph -> X_ x e. I S =/= (/) )

Proof

Step Hyp Ref Expression
1 dfac14lem.i 
 |-  ( ph -> I e. V )
2 dfac14lem.s 
 |-  ( ( ph /\ x e. I ) -> S e. W )
3 dfac14lem.0 
 |-  ( ( ph /\ x e. I ) -> S =/= (/) )
4 dfac14lem.p 
 |-  P = ~P U. S
5 dfac14lem.r 
 |-  R = { y e. ~P ( S u. { P } ) | ( P e. y -> y = ( S u. { P } ) ) }
6 dfac14lem.j 
 |-  J = ( Xt_ ` ( x e. I |-> R ) )
7 dfac14lem.c 
 |-  ( ph -> ( ( cls ` J ) ` X_ x e. I S ) = X_ x e. I ( ( cls ` R ) ` S ) )
8 eleq2w 
 |-  ( y = z -> ( P e. y <-> P e. z ) )
9 eqeq1 
 |-  ( y = z -> ( y = ( S u. { P } ) <-> z = ( S u. { P } ) ) )
10 8 9 imbi12d 
 |-  ( y = z -> ( ( P e. y -> y = ( S u. { P } ) ) <-> ( P e. z -> z = ( S u. { P } ) ) ) )
11 10 5 elrab2 
 |-  ( z e. R <-> ( z e. ~P ( S u. { P } ) /\ ( P e. z -> z = ( S u. { P } ) ) ) )
12 3 adantr 
 |-  ( ( ( ph /\ x e. I ) /\ z e. ~P ( S u. { P } ) ) -> S =/= (/) )
13 ineq1 
 |-  ( z = ( S u. { P } ) -> ( z i^i S ) = ( ( S u. { P } ) i^i S ) )
14 ssun1 
 |-  S C_ ( S u. { P } )
15 sseqin2 
 |-  ( S C_ ( S u. { P } ) <-> ( ( S u. { P } ) i^i S ) = S )
16 14 15 mpbi 
 |-  ( ( S u. { P } ) i^i S ) = S
17 13 16 eqtrdi 
 |-  ( z = ( S u. { P } ) -> ( z i^i S ) = S )
18 17 neeq1d 
 |-  ( z = ( S u. { P } ) -> ( ( z i^i S ) =/= (/) <-> S =/= (/) ) )
19 12 18 syl5ibrcom 
 |-  ( ( ( ph /\ x e. I ) /\ z e. ~P ( S u. { P } ) ) -> ( z = ( S u. { P } ) -> ( z i^i S ) =/= (/) ) )
20 19 imim2d 
 |-  ( ( ( ph /\ x e. I ) /\ z e. ~P ( S u. { P } ) ) -> ( ( P e. z -> z = ( S u. { P } ) ) -> ( P e. z -> ( z i^i S ) =/= (/) ) ) )
21 20 expimpd 
 |-  ( ( ph /\ x e. I ) -> ( ( z e. ~P ( S u. { P } ) /\ ( P e. z -> z = ( S u. { P } ) ) ) -> ( P e. z -> ( z i^i S ) =/= (/) ) ) )
22 11 21 syl5bi 
 |-  ( ( ph /\ x e. I ) -> ( z e. R -> ( P e. z -> ( z i^i S ) =/= (/) ) ) )
23 22 ralrimiv 
 |-  ( ( ph /\ x e. I ) -> A. z e. R ( P e. z -> ( z i^i S ) =/= (/) ) )
24 snex 
 |-  { P } e. _V
25 unexg 
 |-  ( ( S e. W /\ { P } e. _V ) -> ( S u. { P } ) e. _V )
26 2 24 25 sylancl 
 |-  ( ( ph /\ x e. I ) -> ( S u. { P } ) e. _V )
27 ssun2 
 |-  { P } C_ ( S u. { P } )
28 uniexg 
 |-  ( S e. W -> U. S e. _V )
29 pwexg 
 |-  ( U. S e. _V -> ~P U. S e. _V )
30 2 28 29 3syl 
 |-  ( ( ph /\ x e. I ) -> ~P U. S e. _V )
31 4 30 eqeltrid 
 |-  ( ( ph /\ x e. I ) -> P e. _V )
32 snidg 
 |-  ( P e. _V -> P e. { P } )
33 31 32 syl 
 |-  ( ( ph /\ x e. I ) -> P e. { P } )
34 27 33 sselid 
 |-  ( ( ph /\ x e. I ) -> P e. ( S u. { P } ) )
35 epttop 
 |-  ( ( ( S u. { P } ) e. _V /\ P e. ( S u. { P } ) ) -> { y e. ~P ( S u. { P } ) | ( P e. y -> y = ( S u. { P } ) ) } e. ( TopOn ` ( S u. { P } ) ) )
36 26 34 35 syl2anc 
 |-  ( ( ph /\ x e. I ) -> { y e. ~P ( S u. { P } ) | ( P e. y -> y = ( S u. { P } ) ) } e. ( TopOn ` ( S u. { P } ) ) )
37 5 36 eqeltrid 
 |-  ( ( ph /\ x e. I ) -> R e. ( TopOn ` ( S u. { P } ) ) )
38 topontop 
 |-  ( R e. ( TopOn ` ( S u. { P } ) ) -> R e. Top )
39 37 38 syl 
 |-  ( ( ph /\ x e. I ) -> R e. Top )
40 toponuni 
 |-  ( R e. ( TopOn ` ( S u. { P } ) ) -> ( S u. { P } ) = U. R )
41 37 40 syl 
 |-  ( ( ph /\ x e. I ) -> ( S u. { P } ) = U. R )
42 14 41 sseqtrid 
 |-  ( ( ph /\ x e. I ) -> S C_ U. R )
43 34 41 eleqtrd 
 |-  ( ( ph /\ x e. I ) -> P e. U. R )
44 eqid 
 |-  U. R = U. R
45 44 elcls 
 |-  ( ( R e. Top /\ S C_ U. R /\ P e. U. R ) -> ( P e. ( ( cls ` R ) ` S ) <-> A. z e. R ( P e. z -> ( z i^i S ) =/= (/) ) ) )
46 39 42 43 45 syl3anc 
 |-  ( ( ph /\ x e. I ) -> ( P e. ( ( cls ` R ) ` S ) <-> A. z e. R ( P e. z -> ( z i^i S ) =/= (/) ) ) )
47 23 46 mpbird 
 |-  ( ( ph /\ x e. I ) -> P e. ( ( cls ` R ) ` S ) )
48 47 ralrimiva 
 |-  ( ph -> A. x e. I P e. ( ( cls ` R ) ` S ) )
49 mptelixpg 
 |-  ( I e. V -> ( ( x e. I |-> P ) e. X_ x e. I ( ( cls ` R ) ` S ) <-> A. x e. I P e. ( ( cls ` R ) ` S ) ) )
50 1 49 syl 
 |-  ( ph -> ( ( x e. I |-> P ) e. X_ x e. I ( ( cls ` R ) ` S ) <-> A. x e. I P e. ( ( cls ` R ) ` S ) ) )
51 48 50 mpbird 
 |-  ( ph -> ( x e. I |-> P ) e. X_ x e. I ( ( cls ` R ) ` S ) )
52 51 ne0d 
 |-  ( ph -> X_ x e. I ( ( cls ` R ) ` S ) =/= (/) )
53 37 ralrimiva 
 |-  ( ph -> A. x e. I R e. ( TopOn ` ( S u. { P } ) ) )
54 6 pttopon 
 |-  ( ( I e. V /\ A. x e. I R e. ( TopOn ` ( S u. { P } ) ) ) -> J e. ( TopOn ` X_ x e. I ( S u. { P } ) ) )
55 1 53 54 syl2anc 
 |-  ( ph -> J e. ( TopOn ` X_ x e. I ( S u. { P } ) ) )
56 topontop 
 |-  ( J e. ( TopOn ` X_ x e. I ( S u. { P } ) ) -> J e. Top )
57 cls0 
 |-  ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
58 55 56 57 3syl 
 |-  ( ph -> ( ( cls ` J ) ` (/) ) = (/) )
59 52 7 58 3netr4d 
 |-  ( ph -> ( ( cls ` J ) ` X_ x e. I S ) =/= ( ( cls ` J ) ` (/) ) )
60 fveq2 
 |-  ( X_ x e. I S = (/) -> ( ( cls ` J ) ` X_ x e. I S ) = ( ( cls ` J ) ` (/) ) )
61 60 necon3i 
 |-  ( ( ( cls ` J ) ` X_ x e. I S ) =/= ( ( cls ` J ) ` (/) ) -> X_ x e. I S =/= (/) )
62 59 61 syl 
 |-  ( ph -> X_ x e. I S =/= (/) )