Metamath Proof Explorer

Theorem tuslem

Description: Lemma for tusbas , tusunif , and tustopn . (Contributed by Thierry Arnoux, 5-Dec-2017) (Proof shortened by AV, 28-Oct-2024)

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 tsetndxnbasendx 
 |-  ( TopSet ` ndx ) =/= ( Base ` ndx )
4 3 necomi 
 |-  ( Base ` ndx ) =/= ( TopSet ` ndx )
5 2 4 setsnid 
 |-  ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) = ( Base ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
6 ustbas2 
 |-  ( U e. ( UnifOn ` X ) -> X = dom U. U )
7 uniexg 
 |-  ( U e. ( UnifOn ` X ) -> U. U e. _V )
8 dmexg 
 |-  ( U. U e. _V -> dom U. U e. _V )
9 eqid 
 |-  { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } = { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. }
10 basendxltunifndx 
 |-  ( Base ` ndx ) < ( UnifSet ` ndx )
11 unifndxnn 
 |-  ( UnifSet ` ndx ) e. NN
12 9 10 11 2strbas1 
 |-  ( dom U. U e. _V -> dom U. U = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
13 7 8 12 3syl 
 |-  ( U e. ( UnifOn ` X ) -> dom U. U = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
14 6 13 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
15 tusval 
 |-  ( U e. ( UnifOn ` X ) -> ( toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
16 1 15 eqtrid 
 |-  ( U e. ( UnifOn ` X ) -> K = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
17 16 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( Base ` K ) = ( Base ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
18 5 14 17 3eqtr4a 
 |-  ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) )
19 unifid 
 |-  UnifSet = Slot ( UnifSet ` ndx )
20 unifndxntsetndx 
 |-  ( UnifSet ` ndx ) =/= ( TopSet ` ndx )
21 19 20 setsnid 
 |-  ( UnifSet ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) = ( UnifSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
22 9 10 11 19 2strop1 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) )
23 16 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( UnifSet ` K ) = ( UnifSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
24 21 22 23 3eqtr4a 
 |-  ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) )
25 prex 
 |-  { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } e. _V
26 fvex 
 |-  ( unifTop ` U ) e. _V
27 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
28 27 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 ) >. ) ) )
29 25 26 28 mp2an 
 |-  ( unifTop ` U ) = ( TopSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) )
30 16 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( TopSet ` K ) = ( TopSet ` ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) )
31 29 30 eqtr4id 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopSet ` K ) )
32 utopbas 
 |-  ( U e. ( UnifOn ` X ) -> X = U. ( unifTop ` U ) )
33 31 unieqd 
 |-  ( U e. ( UnifOn ` X ) -> U. ( unifTop ` U ) = U. ( TopSet ` K ) )
34 32 18 33 3eqtr3rd 
 |-  ( U e. ( UnifOn ` X ) -> U. ( TopSet ` K ) = ( Base ` K ) )
35 34 oveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( ( TopSet ` K ) |`t ( Base ` K ) ) )
36 fvex 
 |-  ( TopSet ` K ) e. _V
37 eqid 
 |-  U. ( TopSet ` K ) = U. ( TopSet ` K )
38 37 restid 
 |-  ( ( TopSet ` K ) e. _V -> ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( TopSet ` K ) )
39 36 38 ax-mp 
 |-  ( ( TopSet ` K ) |`t U. ( TopSet ` K ) ) = ( TopSet ` K )
40 eqid 
 |-  ( Base ` K ) = ( Base ` K )
41 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
42 40 41 topnval 
 |-  ( ( TopSet ` K ) |`t ( Base ` K ) ) = ( TopOpen ` K )
43 35 39 42 3eqtr3g 
 |-  ( U e. ( UnifOn ` X ) -> ( TopSet ` K ) = ( TopOpen ` K ) )
44 31 43 eqtrd 
 |-  ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) )
45 18 24 44 3jca 
 |-  ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) )