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

Metamath Proof Explorer

Theorem ust0

Description: The unique uniform structure of the empty set is the empty set. Remark 3 of BourbakiTop1 p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ust0 
|- ( UnifOn ` (/) ) = { { (/) } }

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 isust 
 |-  ( (/) e. _V -> ( u e. ( UnifOn ` (/) ) <-> ( u C_ ~P ( (/) X. (/) ) /\ ( (/) X. (/) ) e. u /\ A. v e. u ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` (/) ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) ) )
3 1 2 ax-mp 
 |-  ( u e. ( UnifOn ` (/) ) <-> ( u C_ ~P ( (/) X. (/) ) /\ ( (/) X. (/) ) e. u /\ A. v e. u ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` (/) ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) )
4 3 simp1bi 
 |-  ( u e. ( UnifOn ` (/) ) -> u C_ ~P ( (/) X. (/) ) )
5 0xp 
 |-  ( (/) X. (/) ) = (/)
6 5 pweqi 
 |-  ~P ( (/) X. (/) ) = ~P (/)
7 pw0 
 |-  ~P (/) = { (/) }
8 6 7 eqtri 
 |-  ~P ( (/) X. (/) ) = { (/) }
9 4 8 sseqtrdi 
 |-  ( u e. ( UnifOn ` (/) ) -> u C_ { (/) } )
10 ustbasel 
 |-  ( u e. ( UnifOn ` (/) ) -> ( (/) X. (/) ) e. u )
11 5 10 eqeltrrid 
 |-  ( u e. ( UnifOn ` (/) ) -> (/) e. u )
12 11 snssd 
 |-  ( u e. ( UnifOn ` (/) ) -> { (/) } C_ u )
13 9 12 eqssd 
 |-  ( u e. ( UnifOn ` (/) ) -> u = { (/) } )
14 velsn 
 |-  ( u e. { { (/) } } <-> u = { (/) } )
15 13 14 sylibr 
 |-  ( u e. ( UnifOn ` (/) ) -> u e. { { (/) } } )
16 15 ssriv 
 |-  ( UnifOn ` (/) ) C_ { { (/) } }
17 8 eqimss2i 
 |-  { (/) } C_ ~P ( (/) X. (/) )
18 1 snid 
 |-  (/) e. { (/) }
19 5 18 eqeltri 
 |-  ( (/) X. (/) ) e. { (/) }
20 18 a1i 
 |-  ( (/) C_ (/) -> (/) e. { (/) } )
21 8 raleqi 
 |-  ( A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } ) <-> A. w e. { (/) } ( (/) C_ w -> w e. { (/) } ) )
22 sseq2 
 |-  ( w = (/) -> ( (/) C_ w <-> (/) C_ (/) ) )
23 eleq1 
 |-  ( w = (/) -> ( w e. { (/) } <-> (/) e. { (/) } ) )
24 22 23 imbi12d 
 |-  ( w = (/) -> ( ( (/) C_ w -> w e. { (/) } ) <-> ( (/) C_ (/) -> (/) e. { (/) } ) ) )
25 1 24 ralsn 
 |-  ( A. w e. { (/) } ( (/) C_ w -> w e. { (/) } ) <-> ( (/) C_ (/) -> (/) e. { (/) } ) )
26 21 25 bitri 
 |-  ( A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } ) <-> ( (/) C_ (/) -> (/) e. { (/) } ) )
27 20 26 mpbir 
 |-  A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } )
28 inidm 
 |-  ( (/) i^i (/) ) = (/)
29 28 18 eqeltri 
 |-  ( (/) i^i (/) ) e. { (/) }
30 ineq2 
 |-  ( w = (/) -> ( (/) i^i w ) = ( (/) i^i (/) ) )
31 30 eleq1d 
 |-  ( w = (/) -> ( ( (/) i^i w ) e. { (/) } <-> ( (/) i^i (/) ) e. { (/) } ) )
32 1 31 ralsn 
 |-  ( A. w e. { (/) } ( (/) i^i w ) e. { (/) } <-> ( (/) i^i (/) ) e. { (/) } )
33 29 32 mpbir 
 |-  A. w e. { (/) } ( (/) i^i w ) e. { (/) }
34 res0 
 |-  ( _I |` (/) ) = (/)
35 34 eqimssi 
 |-  ( _I |` (/) ) C_ (/)
36 cnv0 
 |-  `' (/) = (/)
37 36 18 eqeltri 
 |-  `' (/) e. { (/) }
38 0trrel 
 |-  ( (/) o. (/) ) C_ (/)
39 id 
 |-  ( w = (/) -> w = (/) )
40 39 39 coeq12d 
 |-  ( w = (/) -> ( w o. w ) = ( (/) o. (/) ) )
41 40 sseq1d 
 |-  ( w = (/) -> ( ( w o. w ) C_ (/) <-> ( (/) o. (/) ) C_ (/) ) )
42 1 41 rexsn 
 |-  ( E. w e. { (/) } ( w o. w ) C_ (/) <-> ( (/) o. (/) ) C_ (/) )
43 38 42 mpbir 
 |-  E. w e. { (/) } ( w o. w ) C_ (/)
44 35 37 43 3pm3.2i 
 |-  ( ( _I |` (/) ) C_ (/) /\ `' (/) e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ (/) )
45 sseq1 
 |-  ( v = (/) -> ( v C_ w <-> (/) C_ w ) )
46 45 imbi1d 
 |-  ( v = (/) -> ( ( v C_ w -> w e. { (/) } ) <-> ( (/) C_ w -> w e. { (/) } ) ) )
47 46 ralbidv 
 |-  ( v = (/) -> ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) <-> A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } ) ) )
48 ineq1 
 |-  ( v = (/) -> ( v i^i w ) = ( (/) i^i w ) )
49 48 eleq1d 
 |-  ( v = (/) -> ( ( v i^i w ) e. { (/) } <-> ( (/) i^i w ) e. { (/) } ) )
50 49 ralbidv 
 |-  ( v = (/) -> ( A. w e. { (/) } ( v i^i w ) e. { (/) } <-> A. w e. { (/) } ( (/) i^i w ) e. { (/) } ) )
51 sseq2 
 |-  ( v = (/) -> ( ( _I |` (/) ) C_ v <-> ( _I |` (/) ) C_ (/) ) )
52 cnveq 
 |-  ( v = (/) -> `' v = `' (/) )
53 52 eleq1d 
 |-  ( v = (/) -> ( `' v e. { (/) } <-> `' (/) e. { (/) } ) )
54 sseq2 
 |-  ( v = (/) -> ( ( w o. w ) C_ v <-> ( w o. w ) C_ (/) ) )
55 54 rexbidv 
 |-  ( v = (/) -> ( E. w e. { (/) } ( w o. w ) C_ v <-> E. w e. { (/) } ( w o. w ) C_ (/) ) )
56 51 53 55 3anbi123d 
 |-  ( v = (/) -> ( ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) <-> ( ( _I |` (/) ) C_ (/) /\ `' (/) e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ (/) ) ) )
57 47 50 56 3anbi123d 
 |-  ( v = (/) -> ( ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( v i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) ) <-> ( A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( (/) i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ (/) /\ `' (/) e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ (/) ) ) ) )
58 1 57 ralsn 
 |-  ( A. v e. { (/) } ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( v i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) ) <-> ( A. w e. ~P ( (/) X. (/) ) ( (/) C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( (/) i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ (/) /\ `' (/) e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ (/) ) ) )
59 27 33 44 58 mpbir3an 
 |-  A. v e. { (/) } ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( v i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) )
60 isust 
 |-  ( (/) e. _V -> ( { (/) } e. ( UnifOn ` (/) ) <-> ( { (/) } C_ ~P ( (/) X. (/) ) /\ ( (/) X. (/) ) e. { (/) } /\ A. v e. { (/) } ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( v i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) ) ) ) )
61 1 60 ax-mp 
 |-  ( { (/) } e. ( UnifOn ` (/) ) <-> ( { (/) } C_ ~P ( (/) X. (/) ) /\ ( (/) X. (/) ) e. { (/) } /\ A. v e. { (/) } ( A. w e. ~P ( (/) X. (/) ) ( v C_ w -> w e. { (/) } ) /\ A. w e. { (/) } ( v i^i w ) e. { (/) } /\ ( ( _I |` (/) ) C_ v /\ `' v e. { (/) } /\ E. w e. { (/) } ( w o. w ) C_ v ) ) ) )
62 17 19 59 61 mpbir3an 
 |-  { (/) } e. ( UnifOn ` (/) )
63 snssi 
 |-  ( { (/) } e. ( UnifOn ` (/) ) -> { { (/) } } C_ ( UnifOn ` (/) ) )
64 62 63 ax-mp 
 |-  { { (/) } } C_ ( UnifOn ` (/) )
65 16 64 eqssi 
 |-  ( UnifOn ` (/) ) = { { (/) } }