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

Metamath Proof Explorer

Theorem txtube

Description: The "tube lemma". If X is compact and there is an open set U containing the line X X. { A } , then there is a "tube" X X. u for some neighborhood u of A which is entirely contained within U . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses txtube.x 
|- X = U. R
txtube.y 
|- Y = U. S
txtube.r 
|- ( ph -> R e. Comp )
txtube.s 
|- ( ph -> S e. Top )
txtube.w 
|- ( ph -> U e. ( R tX S ) )
txtube.u 
|- ( ph -> ( X X. { A } ) C_ U )
txtube.a 
|- ( ph -> A e. Y )
Assertion txtube 
|- ( ph -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) )

Proof

Step Hyp Ref Expression
1 txtube.x 
 |-  X = U. R
2 txtube.y 
 |-  Y = U. S
3 txtube.r 
 |-  ( ph -> R e. Comp )
4 txtube.s 
 |-  ( ph -> S e. Top )
5 txtube.w 
 |-  ( ph -> U e. ( R tX S ) )
6 txtube.u 
 |-  ( ph -> ( X X. { A } ) C_ U )
7 txtube.a 
 |-  ( ph -> A e. Y )
8 eleq1 
 |-  ( y = <. x , A >. -> ( y e. ( u X. v ) <-> <. x , A >. e. ( u X. v ) ) )
9 8 anbi1d 
 |-  ( y = <. x , A >. -> ( ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) ) )
10 9 2rexbidv 
 |-  ( y = <. x , A >. -> ( E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> E. u e. R E. v e. S ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) ) )
11 eltx 
 |-  ( ( R e. Comp /\ S e. Top ) -> ( U e. ( R tX S ) <-> A. y e. U E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) ) )
12 3 4 11 syl2anc 
 |-  ( ph -> ( U e. ( R tX S ) <-> A. y e. U E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) ) )
13 5 12 mpbid 
 |-  ( ph -> A. y e. U E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) )
14 13 adantr 
 |-  ( ( ph /\ x e. X ) -> A. y e. U E. u e. R E. v e. S ( y e. ( u X. v ) /\ ( u X. v ) C_ U ) )
15 6 adantr 
 |-  ( ( ph /\ x e. X ) -> ( X X. { A } ) C_ U )
16 id 
 |-  ( x e. X -> x e. X )
17 snidg 
 |-  ( A e. Y -> A e. { A } )
18 7 17 syl 
 |-  ( ph -> A e. { A } )
19 opelxpi 
 |-  ( ( x e. X /\ A e. { A } ) -> <. x , A >. e. ( X X. { A } ) )
20 16 18 19 syl2anr 
 |-  ( ( ph /\ x e. X ) -> <. x , A >. e. ( X X. { A } ) )
21 15 20 sseldd 
 |-  ( ( ph /\ x e. X ) -> <. x , A >. e. U )
22 10 14 21 rspcdva 
 |-  ( ( ph /\ x e. X ) -> E. u e. R E. v e. S ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) )
23 opelxp 
 |-  ( <. x , A >. e. ( u X. v ) <-> ( x e. u /\ A e. v ) )
24 23 anbi1i 
 |-  ( ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> ( ( x e. u /\ A e. v ) /\ ( u X. v ) C_ U ) )
25 anass 
 |-  ( ( ( x e. u /\ A e. v ) /\ ( u X. v ) C_ U ) <-> ( x e. u /\ ( A e. v /\ ( u X. v ) C_ U ) ) )
26 24 25 bitri 
 |-  ( ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> ( x e. u /\ ( A e. v /\ ( u X. v ) C_ U ) ) )
27 26 rexbii 
 |-  ( E. v e. S ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> E. v e. S ( x e. u /\ ( A e. v /\ ( u X. v ) C_ U ) ) )
28 r19.42v 
 |-  ( E. v e. S ( x e. u /\ ( A e. v /\ ( u X. v ) C_ U ) ) <-> ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) )
29 27 28 bitri 
 |-  ( E. v e. S ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) )
30 29 rexbii 
 |-  ( E. u e. R E. v e. S ( <. x , A >. e. ( u X. v ) /\ ( u X. v ) C_ U ) <-> E. u e. R ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) )
31 22 30 sylib 
 |-  ( ( ph /\ x e. X ) -> E. u e. R ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) )
32 31 ralrimiva 
 |-  ( ph -> A. x e. X E. u e. R ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) )
33 eleq2 
 |-  ( v = ( f ` u ) -> ( A e. v <-> A e. ( f ` u ) ) )
34 xpeq2 
 |-  ( v = ( f ` u ) -> ( u X. v ) = ( u X. ( f ` u ) ) )
35 34 sseq1d 
 |-  ( v = ( f ` u ) -> ( ( u X. v ) C_ U <-> ( u X. ( f ` u ) ) C_ U ) )
36 33 35 anbi12d 
 |-  ( v = ( f ` u ) -> ( ( A e. v /\ ( u X. v ) C_ U ) <-> ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) )
37 1 36 cmpcovf 
 |-  ( ( R e. Comp /\ A. x e. X E. u e. R ( x e. u /\ E. v e. S ( A e. v /\ ( u X. v ) C_ U ) ) ) -> E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) )
38 3 32 37 syl2anc 
 |-  ( ph -> E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) )
39 rint0 
 |-  ( ran f = (/) -> ( Y i^i |^| ran f ) = Y )
40 39 adantl 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f = (/) ) -> ( Y i^i |^| ran f ) = Y )
41 2 topopn 
 |-  ( S e. Top -> Y e. S )
42 4 41 syl 
 |-  ( ph -> Y e. S )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f = (/) ) -> Y e. S )
44 40 43 eqeltrd 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f = (/) ) -> ( Y i^i |^| ran f ) e. S )
45 4 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> S e. Top )
46 simprrl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> f : t --> S )
47 46 frnd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ran f C_ S )
48 47 adantr 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> ran f C_ S )
49 simpr 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> ran f =/= (/) )
50 simplr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> t e. ( ~P R i^i Fin ) )
51 50 elin2d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> t e. Fin )
52 46 ffnd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> f Fn t )
53 dffn4 
 |-  ( f Fn t <-> f : t -onto-> ran f )
54 52 53 sylib 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> f : t -onto-> ran f )
55 fofi 
 |-  ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f e. Fin )
56 51 54 55 syl2anc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ran f e. Fin )
57 56 adantr 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> ran f e. Fin )
58 fiinopn 
 |-  ( S e. Top -> ( ( ran f C_ S /\ ran f =/= (/) /\ ran f e. Fin ) -> |^| ran f e. S ) )
59 58 imp 
 |-  ( ( S e. Top /\ ( ran f C_ S /\ ran f =/= (/) /\ ran f e. Fin ) ) -> |^| ran f e. S )
60 45 48 49 57 59 syl13anc 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> |^| ran f e. S )
61 elssuni 
 |-  ( |^| ran f e. S -> |^| ran f C_ U. S )
62 60 61 syl 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> |^| ran f C_ U. S )
63 62 2 sseqtrrdi 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> |^| ran f C_ Y )
64 sseqin2 
 |-  ( |^| ran f C_ Y <-> ( Y i^i |^| ran f ) = |^| ran f )
65 63 64 sylib 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> ( Y i^i |^| ran f ) = |^| ran f )
66 65 60 eqeltrd 
 |-  ( ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) /\ ran f =/= (/) ) -> ( Y i^i |^| ran f ) e. S )
67 44 66 pm2.61dane 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ( Y i^i |^| ran f ) e. S )
68 7 ad2antrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A e. Y )
69 simprrr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) )
70 simpl 
 |-  ( ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) -> A e. ( f ` u ) )
71 70 ralimi 
 |-  ( A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) -> A. u e. t A e. ( f ` u ) )
72 69 71 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A. u e. t A e. ( f ` u ) )
73 eliin 
 |-  ( A e. Y -> ( A e. |^|_ u e. t ( f ` u ) <-> A. u e. t A e. ( f ` u ) ) )
74 68 73 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ( A e. |^|_ u e. t ( f ` u ) <-> A. u e. t A e. ( f ` u ) ) )
75 72 74 mpbird 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A e. |^|_ u e. t ( f ` u ) )
76 fniinfv 
 |-  ( f Fn t -> |^|_ u e. t ( f ` u ) = |^| ran f )
77 52 76 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> |^|_ u e. t ( f ` u ) = |^| ran f )
78 75 77 eleqtrd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A e. |^| ran f )
79 68 78 elind 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A e. ( Y i^i |^| ran f ) )
80 simprl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> X = U. t )
81 uniiun 
 |-  U. t = U_ u e. t u
82 80 81 eqtrdi 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> X = U_ u e. t u )
83 82 xpeq1d 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ( X X. ( Y i^i |^| ran f ) ) = ( U_ u e. t u X. ( Y i^i |^| ran f ) ) )
84 xpiundir 
 |-  ( U_ u e. t u X. ( Y i^i |^| ran f ) ) = U_ u e. t ( u X. ( Y i^i |^| ran f ) )
85 83 84 eqtrdi 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ( X X. ( Y i^i |^| ran f ) ) = U_ u e. t ( u X. ( Y i^i |^| ran f ) ) )
86 simpr 
 |-  ( ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) -> ( u X. ( f ` u ) ) C_ U )
87 86 ralimi 
 |-  ( A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) -> A. u e. t ( u X. ( f ` u ) ) C_ U )
88 69 87 syl 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A. u e. t ( u X. ( f ` u ) ) C_ U )
89 inss2 
 |-  ( Y i^i |^| ran f ) C_ |^| ran f
90 76 adantr 
 |-  ( ( f Fn t /\ u e. t ) -> |^|_ u e. t ( f ` u ) = |^| ran f )
91 iinss2 
 |-  ( u e. t -> |^|_ u e. t ( f ` u ) C_ ( f ` u ) )
92 91 adantl 
 |-  ( ( f Fn t /\ u e. t ) -> |^|_ u e. t ( f ` u ) C_ ( f ` u ) )
93 90 92 eqsstrrd 
 |-  ( ( f Fn t /\ u e. t ) -> |^| ran f C_ ( f ` u ) )
94 89 93 sstrid 
 |-  ( ( f Fn t /\ u e. t ) -> ( Y i^i |^| ran f ) C_ ( f ` u ) )
95 xpss2 
 |-  ( ( Y i^i |^| ran f ) C_ ( f ` u ) -> ( u X. ( Y i^i |^| ran f ) ) C_ ( u X. ( f ` u ) ) )
96 sstr2 
 |-  ( ( u X. ( Y i^i |^| ran f ) ) C_ ( u X. ( f ` u ) ) -> ( ( u X. ( f ` u ) ) C_ U -> ( u X. ( Y i^i |^| ran f ) ) C_ U ) )
97 94 95 96 3syl 
 |-  ( ( f Fn t /\ u e. t ) -> ( ( u X. ( f ` u ) ) C_ U -> ( u X. ( Y i^i |^| ran f ) ) C_ U ) )
98 97 ralimdva 
 |-  ( f Fn t -> ( A. u e. t ( u X. ( f ` u ) ) C_ U -> A. u e. t ( u X. ( Y i^i |^| ran f ) ) C_ U ) )
99 52 88 98 sylc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> A. u e. t ( u X. ( Y i^i |^| ran f ) ) C_ U )
100 iunss 
 |-  ( U_ u e. t ( u X. ( Y i^i |^| ran f ) ) C_ U <-> A. u e. t ( u X. ( Y i^i |^| ran f ) ) C_ U )
101 99 100 sylibr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> U_ u e. t ( u X. ( Y i^i |^| ran f ) ) C_ U )
102 85 101 eqsstrd 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> ( X X. ( Y i^i |^| ran f ) ) C_ U )
103 eleq2 
 |-  ( u = ( Y i^i |^| ran f ) -> ( A e. u <-> A e. ( Y i^i |^| ran f ) ) )
104 xpeq2 
 |-  ( u = ( Y i^i |^| ran f ) -> ( X X. u ) = ( X X. ( Y i^i |^| ran f ) ) )
105 104 sseq1d 
 |-  ( u = ( Y i^i |^| ran f ) -> ( ( X X. u ) C_ U <-> ( X X. ( Y i^i |^| ran f ) ) C_ U ) )
106 103 105 anbi12d 
 |-  ( u = ( Y i^i |^| ran f ) -> ( ( A e. u /\ ( X X. u ) C_ U ) <-> ( A e. ( Y i^i |^| ran f ) /\ ( X X. ( Y i^i |^| ran f ) ) C_ U ) ) )
107 106 rspcev 
 |-  ( ( ( Y i^i |^| ran f ) e. S /\ ( A e. ( Y i^i |^| ran f ) /\ ( X X. ( Y i^i |^| ran f ) ) C_ U ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) )
108 67 79 102 107 syl12anc 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ ( X = U. t /\ ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) )
109 108 expr 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ X = U. t ) -> ( ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) ) )
110 109 exlimdv 
 |-  ( ( ( ph /\ t e. ( ~P R i^i Fin ) ) /\ X = U. t ) -> ( E. f ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) ) )
111 110 expimpd 
 |-  ( ( ph /\ t e. ( ~P R i^i Fin ) ) -> ( ( X = U. t /\ E. f ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) ) )
112 111 rexlimdva 
 |-  ( ph -> ( E. t e. ( ~P R i^i Fin ) ( X = U. t /\ E. f ( f : t --> S /\ A. u e. t ( A e. ( f ` u ) /\ ( u X. ( f ` u ) ) C_ U ) ) ) -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) ) )
113 38 112 mpd 
 |-  ( ph -> E. u e. S ( A e. u /\ ( X X. u ) C_ U ) )