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 ` (/) ) = { { (/) } }