Metamath Proof Explorer

Theorem tuslem

Description: Lemma for tusbas , tusunif , and tustopn . (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Hypothesis tuslem.k 
|- K = ( toUnifSp ` U )
Assertion tuslem 
|- ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )

Proof

Step Hyp Ref Expression
1 tuslem.k 
 |-  K = ( toUnifSp ` U )
2 baseid 
 |-  Base = Slot ( Base ` ndx )
3 1re 
 |-  1 e. RR
4 1lt9 
 |-  1 < 9
5 3 4 ltneii 
 |-  1 =/= 9
6 basendx 
 |-  ( Base ` ndx ) = 1
7 tsetndx 
 |-  ( TopSet ` ndx ) = 9
8 6 7 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( TopSet ` ndx ) <-> 1 =/= 9 )
9 5 8 mpbir 
 |-  ( Base ` ndx ) =/= ( TopSet ` ndx )
10 2 9 setsnid 
 |-  ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) = ( Base ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
11 ustbas2 
 |-  ( U e. ( UnifOn ` X ) -> X = dom U. U )
12 uniexg 
 |-  ( U e. ( UnifOn ` X ) -> U. U e. _V )
13 dmexg 
 |-  ( U. U e. _V -> dom U. U e. _V )
14 eqid 
 |-  { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } = { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. }
15 df-unif 
 |-  UnifSet = Slot ; 1 3
16 1nn 
 |-  1 e. NN
17 3nn0 
 |-  3 e. NN0
18 1nn0 
 |-  1 e. NN0
19 1lt10 
 |-  1 < ; 1 0
20 16 17 18 19 declti 
 |-  1 < ; 1 3
21 3nn 
 |-  3 e. NN
22 18 21 decnncl 
 |-  ; 1 3 e. NN
23 14 15 20 22 2strbas 
 |-  ( dom U. U e. _V -> dom U. U = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
24 12 13 23 3syl 
 |-  ( U e. ( UnifOn ` X ) -> dom U. U = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
25 11 24 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
26 tusval 
 |-  ( U e. ( UnifOn ` X ) -> ( toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
27 1 26 syl5eq 
 |-  ( U e. ( UnifOn ` X ) -> K = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
28 27 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( Base ` K ) = ( Base ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
29 10 25 28 3eqtr4a 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) )
30 unifid 
 |-  UnifSet = Slot ( UnifSet ` ndx )
31 9re 
 |-  9 e. RR
32 9nn0 
 |-  9 e. NN0
33 9lt10 
 |-  9 < ; 1 0
34 16 17 32 33 declti 
 |-  9 < ; 1 3
35 31 34 gtneii 
 |-  ; 1 3 =/= 9
36 unifndx 
 |-  ( UnifSet ` ndx ) = ; 1 3
37 36 7 neeq12i 
 |-  ( ( UnifSet ` ndx ) =/= ( TopSet ` ndx ) <-> ; 1 3 =/= 9 )
38 35 37 mpbir 
 |-  ( UnifSet ` ndx ) =/= ( TopSet ` ndx )
39 30 38 setsnid 
 |-  ( UnifSet ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) = ( UnifSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
40 14 15 20 22 2strop 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
41 27 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( UnifSet ` K ) = ( UnifSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
42 39 40 41 3eqtr4a 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) )
43 prex 
 |-  { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } e. _V
44 fvex 
 |-  ( unifTop ` U ) e. _V
45 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
46 45 setsid 
 |-  ( ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } e. _V /\ ( unifTop ` U ) e. _V ) -> ( unifTop ` U ) = ( TopSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
47 43 44 46 mp2an 
 |-  ( unifTop ` U ) = ( TopSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
48 27 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( TopSet ` K ) = ( TopSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
49 47 48 eqtr4id 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopSet ` K ) )
50 utopbas 
 |-  ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )
51 49 unieqd 
 |-  ( U e. ( UnifOn ` X ) -> U. ( unifTop ` U ) = U. ( TopSet ` K ) )
52 50 29 51 3eqtr3rd 
 |-  ( U e. ( UnifOn ` X ) -> U. ( TopSet ` K ) = ( Base ` K ) )
53 52 oveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( ( TopSet ` K ) |`t ( Base ` K ) ) )
54 fvex 
 |-  ( TopSet ` K ) e. _V
55 eqid 
 |-  U. ( TopSet ` K ) = U. ( TopSet ` K )
56 55 restid 
 |-  ( ( TopSet ` K ) e. _V -> ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( TopSet ` K ) )
57 54 56 ax-mp 
 |-  ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( TopSet ` K )
58 eqid 
 |-  ( Base ` K ) = ( Base ` K )
59 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
60 58 59 topnval 
 |-  ( ( TopSet ` K ) |`t ( Base ` K ) ) = ( TopOpen ` K )
61 53 57 60 3eqtr3g 
 |-  ( U e. ( UnifOn ` X ) -> ( TopSet ` K ) = ( TopOpen ` K ) )
62 49 61 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
63 29 42 62 3jca 
 |-  ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )