This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustfilxp

Description: A uniform structure on a nonempty base is a filter. Remark 3 of BourbakiTop1 p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ustfilxp 
|- ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> U e. ( Fil ` ( X X. X ) ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( U e. ( UnifOn ` X ) -> X e. _V )
2 isust 
 |-  ( X e. _V -> ( U e. ( UnifOn ` X ) <-> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) )
3 1 2 syl 
 |-  ( U e. ( UnifOn ` X ) -> ( U e. ( UnifOn ` X ) <-> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) )
4 3 ibi 
 |-  ( U e. ( UnifOn ` X ) -> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) )
5 4 adantl 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) )
6 5 simp1d 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> U C_ ~P ( X X. X ) )
7 5 simp2d 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> ( X X. X ) e. U )
8 7 ne0d 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> U =/= (/) )
9 5 simp3d 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) )
10 9 r19.21bi 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) )
11 10 simp3d 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) )
12 11 simp1d 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> ( _I |` X ) C_ v )
13 opelidres 
 |-  ( w e. _V -> ( <. w , w >. e. ( _I |` X ) <-> w e. X ) )
14 13 elv 
 |-  ( <. w , w >. e. ( _I |` X ) <-> w e. X )
15 14 biimpri 
 |-  ( w e. X -> <. w , w >. e. ( _I |` X ) )
16 15 rgen 
 |-  A. w e. X <. w , w >. e. ( _I |` X )
17 r19.2z 
 |-  ( ( X =/= (/) /\ A. w e. X <. w , w >. e. ( _I |` X ) ) -> E. w e. X <. w , w >. e. ( _I |` X ) )
18 16 17 mpan2 
 |-  ( X =/= (/) -> E. w e. X <. w , w >. e. ( _I |` X ) )
19 18 ad2antrr 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> E. w e. X <. w , w >. e. ( _I |` X ) )
20 ne0i 
 |-  ( <. w , w >. e. ( _I |` X ) -> ( _I |` X ) =/= (/) )
21 20 rexlimivw 
 |-  ( E. w e. X <. w , w >. e. ( _I |` X ) -> ( _I |` X ) =/= (/) )
22 19 21 syl 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> ( _I |` X ) =/= (/) )
23 ssn0 
 |-  ( ( ( _I |` X ) C_ v /\ ( _I |` X ) =/= (/) ) -> v =/= (/) )
24 12 22 23 syl2anc 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> v =/= (/) )
25 24 nelrdva 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> -. (/) e. U )
26 df-nel 
 |-  ( (/) e/ U <-> -. (/) e. U )
27 25 26 sylibr 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> (/) e/ U )
28 10 simp2d 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> A. w e. U ( v i^i w ) e. U )
29 28 r19.21bi 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) /\ w e. U ) -> ( v i^i w ) e. U )
30 vex 
 |-  w e. _V
31 30 inex2 
 |-  ( v i^i w ) e. _V
32 31 pwid 
 |-  ( v i^i w ) e. ~P ( v i^i w )
33 32 a1i 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) /\ w e. U ) -> ( v i^i w ) e. ~P ( v i^i w ) )
34 29 33 elind 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) /\ w e. U ) -> ( v i^i w ) e. ( U i^i ~P ( v i^i w ) ) )
35 34 ne0d 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) /\ w e. U ) -> ( U i^i ~P ( v i^i w ) ) =/= (/) )
36 35 ralrimiva 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) )
37 36 ralrimiva 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> A. v e. U A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) )
38 8 27 37 3jca 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> ( U =/= (/) /\ (/) e/ U /\ A. v e. U A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) ) )
39 1 1 xpexd 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) e. _V )
40 isfbas 
 |-  ( ( X X. X ) e. _V -> ( U e. ( fBas ` ( X X. X ) ) <-> ( U C_ ~P ( X X. X ) /\ ( U =/= (/) /\ (/) e/ U /\ A. v e. U A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) ) ) ) )
41 39 40 syl 
 |-  ( U e. ( UnifOn ` X ) -> ( U e. ( fBas ` ( X X. X ) ) <-> ( U C_ ~P ( X X. X ) /\ ( U =/= (/) /\ (/) e/ U /\ A. v e. U A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) ) ) ) )
42 41 adantl 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> ( U e. ( fBas ` ( X X. X ) ) <-> ( U C_ ~P ( X X. X ) /\ ( U =/= (/) /\ (/) e/ U /\ A. v e. U A. w e. U ( U i^i ~P ( v i^i w ) ) =/= (/) ) ) ) )
43 6 38 42 mpbir2and 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> U e. ( fBas ` ( X X. X ) ) )
44 n0 
 |-  ( ( U i^i ~P w ) =/= (/) <-> E. v v e. ( U i^i ~P w ) )
45 elin 
 |-  ( v e. ( U i^i ~P w ) <-> ( v e. U /\ v e. ~P w ) )
46 velpw 
 |-  ( v e. ~P w <-> v C_ w )
47 46 anbi2i 
 |-  ( ( v e. U /\ v e. ~P w ) <-> ( v e. U /\ v C_ w ) )
48 45 47 bitri 
 |-  ( v e. ( U i^i ~P w ) <-> ( v e. U /\ v C_ w ) )
49 48 exbii 
 |-  ( E. v v e. ( U i^i ~P w ) <-> E. v ( v e. U /\ v C_ w ) )
50 44 49 bitri 
 |-  ( ( U i^i ~P w ) =/= (/) <-> E. v ( v e. U /\ v C_ w ) )
51 10 simp1d 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) -> A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) )
52 51 r19.21bi 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ v e. U ) /\ w e. ~P ( X X. X ) ) -> ( v C_ w -> w e. U ) )
53 52 an32s 
 |-  ( ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ w e. ~P ( X X. X ) ) /\ v e. U ) -> ( v C_ w -> w e. U ) )
54 53 expimpd 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ w e. ~P ( X X. X ) ) -> ( ( v e. U /\ v C_ w ) -> w e. U ) )
55 54 exlimdv 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ w e. ~P ( X X. X ) ) -> ( E. v ( v e. U /\ v C_ w ) -> w e. U ) )
56 50 55 biimtrid 
 |-  ( ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) /\ w e. ~P ( X X. X ) ) -> ( ( U i^i ~P w ) =/= (/) -> w e. U ) )
57 56 ralrimiva 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> A. w e. ~P ( X X. X ) ( ( U i^i ~P w ) =/= (/) -> w e. U ) )
58 isfil 
 |-  ( U e. ( Fil ` ( X X. X ) ) <-> ( U e. ( fBas ` ( X X. X ) ) /\ A. w e. ~P ( X X. X ) ( ( U i^i ~P w ) =/= (/) -> w e. U ) ) )
59 43 57 58 sylanbrc 
 |-  ( ( X =/= (/) /\ U e. ( UnifOn ` X ) ) -> U e. ( Fil ` ( X X. X ) ) )