Metamath Proof Explorer

Theorem smfpimbor1lem1

Description: Every open set belongs to T . This is the second step in the proof of Proposition 121E (f) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimbor1lem1.s 
|- ( ph -> S e. SAlg )
smfpimbor1lem1.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfpimbor1lem1.a 
|- D = dom F
smfpimbor1lem1.j 
|- J = ( topGen ` ran (,) )
smfpimbor1lem1.8 
|- ( ph -> G e. J )
smfpimbor1lem1.t 
|- T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
Assertion smfpimbor1lem1 
|- ( ph -> G e. T )

Proof

Step Hyp Ref Expression
1 smfpimbor1lem1.s 
 |-  ( ph -> S e. SAlg )
2 smfpimbor1lem1.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfpimbor1lem1.a 
 |-  D = dom F
4 smfpimbor1lem1.j 
 |-  J = ( topGen ` ran (,) )
5 smfpimbor1lem1.8 
 |-  ( ph -> G e. J )
6 smfpimbor1lem1.t 
 |-  T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
7 4 5 tgqioo2 
 |-  ( ph -> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) )
8 simprr 
 |-  ( ( ph /\ ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) ) -> G = U. q )
9 1 2 3 6 smfresal 
 |-  ( ph -> T e. SAlg )
10 9 adantr 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> T e. SAlg )
11 iooex 
 |-  (,) e. _V
12 11 imaexi 
 |-  ( (,) " ( QQ X. QQ ) ) e. _V
13 12 a1i 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) e. _V )
14 id 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> q C_ ( (,) " ( QQ X. QQ ) ) )
15 13 14 ssexd 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> q e. _V )
16 15 adantl 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> q e. _V )
17 simpr 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> q C_ ( (,) " ( QQ X. QQ ) ) )
18 ioofun 
 |-  Fun (,)
19 18 a1i 
 |-  ( q e. ( (,) " ( QQ X. QQ ) ) -> Fun (,) )
20 id 
 |-  ( q e. ( (,) " ( QQ X. QQ ) ) -> q e. ( (,) " ( QQ X. QQ ) ) )
21 fvelima 
 |-  ( ( Fun (,) /\ q e. ( (,) " ( QQ X. QQ ) ) ) -> E. p e. ( QQ X. QQ ) ( (,) ` p ) = q )
22 19 20 21 syl2anc 
 |-  ( q e. ( (,) " ( QQ X. QQ ) ) -> E. p e. ( QQ X. QQ ) ( (,) ` p ) = q )
23 22 adantl 
 |-  ( ( ph /\ q e. ( (,) " ( QQ X. QQ ) ) ) -> E. p e. ( QQ X. QQ ) ( (,) ` p ) = q )
24 id 
 |-  ( ( (,) ` p ) = q -> ( (,) ` p ) = q )
25 24 eqcomd 
 |-  ( ( (,) ` p ) = q -> q = ( (,) ` p ) )
26 25 adantl 
 |-  ( ( p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> q = ( (,) ` p ) )
27 1st2nd2 
 |-  ( p e. ( QQ X. QQ ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
28 27 fveq2d 
 |-  ( p e. ( QQ X. QQ ) -> ( (,) ` p ) = ( (,) ` <. ( 1st ` p ) , ( 2nd ` p ) >. ) )
29 df-ov 
 |-  ( ( 1st ` p ) (,) ( 2nd ` p ) ) = ( (,) ` <. ( 1st ` p ) , ( 2nd ` p ) >. )
30 29 eqcomi 
 |-  ( (,) ` <. ( 1st ` p ) , ( 2nd ` p ) >. ) = ( ( 1st ` p ) (,) ( 2nd ` p ) )
31 30 a1i 
 |-  ( p e. ( QQ X. QQ ) -> ( (,) ` <. ( 1st ` p ) , ( 2nd ` p ) >. ) = ( ( 1st ` p ) (,) ( 2nd ` p ) ) )
32 28 31 eqtrd 
 |-  ( p e. ( QQ X. QQ ) -> ( (,) ` p ) = ( ( 1st ` p ) (,) ( 2nd ` p ) ) )
33 32 adantr 
 |-  ( ( p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> ( (,) ` p ) = ( ( 1st ` p ) (,) ( 2nd ` p ) ) )
34 26 33 eqtrd 
 |-  ( ( p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> q = ( ( 1st ` p ) (,) ( 2nd ` p ) ) )
35 34 3adant1 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> q = ( ( 1st ` p ) (,) ( 2nd ` p ) ) )
36 ioossre 
 |-  ( ( 1st ` p ) (,) ( 2nd ` p ) ) C_ RR
37 ovex 
 |-  ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. _V
38 37 elpw 
 |-  ( ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. ~P RR <-> ( ( 1st ` p ) (,) ( 2nd ` p ) ) C_ RR )
39 36 38 mpbir 
 |-  ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. ~P RR
40 39 a1i 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. ~P RR )
41 1 adantr 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> S e. SAlg )
42 2 adantr 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> F e. ( SMblFn ` S ) )
43 xp1st 
 |-  ( p e. ( QQ X. QQ ) -> ( 1st ` p ) e. QQ )
44 43 qred 
 |-  ( p e. ( QQ X. QQ ) -> ( 1st ` p ) e. RR )
45 44 rexrd 
 |-  ( p e. ( QQ X. QQ ) -> ( 1st ` p ) e. RR* )
46 45 adantl 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( 1st ` p ) e. RR* )
47 xp2nd 
 |-  ( p e. ( QQ X. QQ ) -> ( 2nd ` p ) e. QQ )
48 47 qred 
 |-  ( p e. ( QQ X. QQ ) -> ( 2nd ` p ) e. RR )
49 48 rexrd 
 |-  ( p e. ( QQ X. QQ ) -> ( 2nd ` p ) e. RR* )
50 49 adantl 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( 2nd ` p ) e. RR* )
51 41 42 3 46 50 smfpimioo 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( `' F " ( ( 1st ` p ) (,) ( 2nd ` p ) ) ) e. ( S |`t D ) )
52 40 51 jca 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. ~P RR /\ ( `' F " ( ( 1st ` p ) (,) ( 2nd ` p ) ) ) e. ( S |`t D ) ) )
53 imaeq2 
 |-  ( e = ( ( 1st ` p ) (,) ( 2nd ` p ) ) -> ( `' F " e ) = ( `' F " ( ( 1st ` p ) (,) ( 2nd ` p ) ) ) )
54 53 eleq1d 
 |-  ( e = ( ( 1st ` p ) (,) ( 2nd ` p ) ) -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " ( ( 1st ` p ) (,) ( 2nd ` p ) ) ) e. ( S |`t D ) ) )
55 54 6 elrab2 
 |-  ( ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. T <-> ( ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. ~P RR /\ ( `' F " ( ( 1st ` p ) (,) ( 2nd ` p ) ) ) e. ( S |`t D ) ) )
56 52 55 sylibr 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) ) -> ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. T )
57 56 3adant3 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> ( ( 1st ` p ) (,) ( 2nd ` p ) ) e. T )
58 35 57 eqeltrd 
 |-  ( ( ph /\ p e. ( QQ X. QQ ) /\ ( (,) ` p ) = q ) -> q e. T )
59 58 3exp 
 |-  ( ph -> ( p e. ( QQ X. QQ ) -> ( ( (,) ` p ) = q -> q e. T ) ) )
60 59 rexlimdv 
 |-  ( ph -> ( E. p e. ( QQ X. QQ ) ( (,) ` p ) = q -> q e. T ) )
61 60 adantr 
 |-  ( ( ph /\ q e. ( (,) " ( QQ X. QQ ) ) ) -> ( E. p e. ( QQ X. QQ ) ( (,) ` p ) = q -> q e. T ) )
62 23 61 mpd 
 |-  ( ( ph /\ q e. ( (,) " ( QQ X. QQ ) ) ) -> q e. T )
63 62 ssd 
 |-  ( ph -> ( (,) " ( QQ X. QQ ) ) C_ T )
64 63 adantr 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> ( (,) " ( QQ X. QQ ) ) C_ T )
65 17 64 sstrd 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> q C_ T )
66 16 65 elpwd 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> q e. ~P T )
67 ssdomg 
 |-  ( ( (,) " ( QQ X. QQ ) ) e. _V -> ( q C_ ( (,) " ( QQ X. QQ ) ) -> q ~<_ ( (,) " ( QQ X. QQ ) ) ) )
68 12 67 ax-mp 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> q ~<_ ( (,) " ( QQ X. QQ ) ) )
69 qct 
 |-  QQ ~<_ _om
70 69 69 pm3.2i 
 |-  ( QQ ~<_ _om /\ QQ ~<_ _om )
71 xpct 
 |-  ( ( QQ ~<_ _om /\ QQ ~<_ _om ) -> ( QQ X. QQ ) ~<_ _om )
72 70 71 ax-mp 
 |-  ( QQ X. QQ ) ~<_ _om
73 fimact 
 |-  ( ( ( QQ X. QQ ) ~<_ _om /\ Fun (,) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ _om )
74 72 18 73 mp2an 
 |-  ( (,) " ( QQ X. QQ ) ) ~<_ _om
75 74 a1i 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> ( (,) " ( QQ X. QQ ) ) ~<_ _om )
76 domtr 
 |-  ( ( q ~<_ ( (,) " ( QQ X. QQ ) ) /\ ( (,) " ( QQ X. QQ ) ) ~<_ _om ) -> q ~<_ _om )
77 68 75 76 syl2anc 
 |-  ( q C_ ( (,) " ( QQ X. QQ ) ) -> q ~<_ _om )
78 77 adantl 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> q ~<_ _om )
79 10 66 78 salunicl 
 |-  ( ( ph /\ q C_ ( (,) " ( QQ X. QQ ) ) ) -> U. q e. T )
80 79 adantrr 
 |-  ( ( ph /\ ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) ) -> U. q e. T )
81 8 80 eqeltrd 
 |-  ( ( ph /\ ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) ) -> G e. T )
82 81 ex 
 |-  ( ph -> ( ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) -> G e. T ) )
83 82 exlimdv 
 |-  ( ph -> ( E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ G = U. q ) -> G e. T ) )
84 7 83 mpd 
 |-  ( ph -> G e. T )