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

Metamath Proof Explorer

Theorem lbsextlem2

Description: Lemma for lbsext . Since A is a chain (actually, we only need it to be closed under binary union), the union T of the spans of each individual element of A is a subspace, and it contains all of U. A (except for our target vector x - we are trying to make x a linear combination of all the other vectors in some set from A ). (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v 
|- V = ( Base ` W )
lbsext.j 
|- J = ( LBasis ` W )
lbsext.n 
|- N = ( LSpan ` W )
lbsext.w 
|- ( ph -> W e. LVec )
lbsext.c 
|- ( ph -> C C_ V )
lbsext.x 
|- ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
lbsext.s 
|- S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
lbsext.p 
|- P = ( LSubSp ` W )
lbsext.a 
|- ( ph -> A C_ S )
lbsext.z 
|- ( ph -> A =/= (/) )
lbsext.r 
|- ( ph -> [C.] Or A )
lbsext.t 
|- T = U_ u e. A ( N ` ( u \ { x } ) )
Assertion lbsextlem2 
|- ( ph -> ( T e. P /\ ( U. A \ { x } ) C_ T ) )

Proof

Step Hyp Ref Expression
1 lbsext.v 
 |-  V = ( Base ` W )
2 lbsext.j 
 |-  J = ( LBasis ` W )
3 lbsext.n 
 |-  N = ( LSpan ` W )
4 lbsext.w 
 |-  ( ph -> W e. LVec )
5 lbsext.c 
 |-  ( ph -> C C_ V )
6 lbsext.x 
 |-  ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
7 lbsext.s 
 |-  S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
8 lbsext.p 
 |-  P = ( LSubSp ` W )
9 lbsext.a 
 |-  ( ph -> A C_ S )
10 lbsext.z 
 |-  ( ph -> A =/= (/) )
11 lbsext.r 
 |-  ( ph -> [C.] Or A )
12 lbsext.t 
 |-  T = U_ u e. A ( N ` ( u \ { x } ) )
13 eqidd 
 |-  ( ph -> ( Scalar ` W ) = ( Scalar ` W ) )
14 eqidd 
 |-  ( ph -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
15 1 a1i 
 |-  ( ph -> V = ( Base ` W ) )
16 eqidd 
 |-  ( ph -> ( +g ` W ) = ( +g ` W ) )
17 eqidd 
 |-  ( ph -> ( .s ` W ) = ( .s ` W ) )
18 8 a1i 
 |-  ( ph -> P = ( LSubSp ` W ) )
19 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
20 4 19 syl 
 |-  ( ph -> W e. LMod )
21 7 ssrab3 
 |-  S C_ ~P V
22 9 21 sstrdi 
 |-  ( ph -> A C_ ~P V )
23 22 sselda 
 |-  ( ( ph /\ u e. A ) -> u e. ~P V )
24 23 elpwid 
 |-  ( ( ph /\ u e. A ) -> u C_ V )
25 24 ssdifssd 
 |-  ( ( ph /\ u e. A ) -> ( u \ { x } ) C_ V )
26 1 3 lspssv 
 |-  ( ( W e. LMod /\ ( u \ { x } ) C_ V ) -> ( N ` ( u \ { x } ) ) C_ V )
27 20 25 26 syl2an2r 
 |-  ( ( ph /\ u e. A ) -> ( N ` ( u \ { x } ) ) C_ V )
28 27 ralrimiva 
 |-  ( ph -> A. u e. A ( N ` ( u \ { x } ) ) C_ V )
29 iunss 
 |-  ( U_ u e. A ( N ` ( u \ { x } ) ) C_ V <-> A. u e. A ( N ` ( u \ { x } ) ) C_ V )
30 28 29 sylibr 
 |-  ( ph -> U_ u e. A ( N ` ( u \ { x } ) ) C_ V )
31 12 30 eqsstrid 
 |-  ( ph -> T C_ V )
32 12 a1i 
 |-  ( ph -> T = U_ u e. A ( N ` ( u \ { x } ) ) )
33 1 8 3 lspcl 
 |-  ( ( W e. LMod /\ ( u \ { x } ) C_ V ) -> ( N ` ( u \ { x } ) ) e. P )
34 20 25 33 syl2an2r 
 |-  ( ( ph /\ u e. A ) -> ( N ` ( u \ { x } ) ) e. P )
35 8 lssn0 
 |-  ( ( N ` ( u \ { x } ) ) e. P -> ( N ` ( u \ { x } ) ) =/= (/) )
36 34 35 syl 
 |-  ( ( ph /\ u e. A ) -> ( N ` ( u \ { x } ) ) =/= (/) )
37 36 ralrimiva 
 |-  ( ph -> A. u e. A ( N ` ( u \ { x } ) ) =/= (/) )
38 r19.2z 
 |-  ( ( A =/= (/) /\ A. u e. A ( N ` ( u \ { x } ) ) =/= (/) ) -> E. u e. A ( N ` ( u \ { x } ) ) =/= (/) )
39 10 37 38 syl2anc 
 |-  ( ph -> E. u e. A ( N ` ( u \ { x } ) ) =/= (/) )
40 iunn0 
 |-  ( E. u e. A ( N ` ( u \ { x } ) ) =/= (/) <-> U_ u e. A ( N ` ( u \ { x } ) ) =/= (/) )
41 39 40 sylib 
 |-  ( ph -> U_ u e. A ( N ` ( u \ { x } ) ) =/= (/) )
42 32 41 eqnetrd 
 |-  ( ph -> T =/= (/) )
43 12 eleq2i 
 |-  ( v e. T <-> v e. U_ u e. A ( N ` ( u \ { x } ) ) )
44 eliun 
 |-  ( v e. U_ u e. A ( N ` ( u \ { x } ) ) <-> E. u e. A v e. ( N ` ( u \ { x } ) ) )
45 difeq1 
 |-  ( u = m -> ( u \ { x } ) = ( m \ { x } ) )
46 45 fveq2d 
 |-  ( u = m -> ( N ` ( u \ { x } ) ) = ( N ` ( m \ { x } ) ) )
47 46 eleq2d 
 |-  ( u = m -> ( v e. ( N ` ( u \ { x } ) ) <-> v e. ( N ` ( m \ { x } ) ) ) )
48 47 cbvrexvw 
 |-  ( E. u e. A v e. ( N ` ( u \ { x } ) ) <-> E. m e. A v e. ( N ` ( m \ { x } ) ) )
49 43 44 48 3bitri 
 |-  ( v e. T <-> E. m e. A v e. ( N ` ( m \ { x } ) ) )
50 12 eleq2i 
 |-  ( w e. T <-> w e. U_ u e. A ( N ` ( u \ { x } ) ) )
51 eliun 
 |-  ( w e. U_ u e. A ( N ` ( u \ { x } ) ) <-> E. u e. A w e. ( N ` ( u \ { x } ) ) )
52 difeq1 
 |-  ( u = n -> ( u \ { x } ) = ( n \ { x } ) )
53 52 fveq2d 
 |-  ( u = n -> ( N ` ( u \ { x } ) ) = ( N ` ( n \ { x } ) ) )
54 53 eleq2d 
 |-  ( u = n -> ( w e. ( N ` ( u \ { x } ) ) <-> w e. ( N ` ( n \ { x } ) ) ) )
55 54 cbvrexvw 
 |-  ( E. u e. A w e. ( N ` ( u \ { x } ) ) <-> E. n e. A w e. ( N ` ( n \ { x } ) ) )
56 50 51 55 3bitri 
 |-  ( w e. T <-> E. n e. A w e. ( N ` ( n \ { x } ) ) )
57 49 56 anbi12i 
 |-  ( ( v e. T /\ w e. T ) <-> ( E. m e. A v e. ( N ` ( m \ { x } ) ) /\ E. n e. A w e. ( N ` ( n \ { x } ) ) ) )
58 reeanv 
 |-  ( E. m e. A E. n e. A ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) <-> ( E. m e. A v e. ( N ` ( m \ { x } ) ) /\ E. n e. A w e. ( N ` ( n \ { x } ) ) ) )
59 57 58 bitr4i 
 |-  ( ( v e. T /\ w e. T ) <-> E. m e. A E. n e. A ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) )
60 simp1l 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ph )
61 60 11 syl 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> [C.] Or A )
62 simp2 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( m e. A /\ n e. A ) )
63 sorpssun 
 |-  ( ( [C.] Or A /\ ( m e. A /\ n e. A ) ) -> ( m u. n ) e. A )
64 61 62 63 syl2anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( m u. n ) e. A )
65 60 20 syl 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> W e. LMod )
66 elssuni 
 |-  ( ( m u. n ) e. A -> ( m u. n ) C_ U. A )
67 64 66 syl 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( m u. n ) C_ U. A )
68 sspwuni 
 |-  ( A C_ ~P V <-> U. A C_ V )
69 22 68 sylib 
 |-  ( ph -> U. A C_ V )
70 60 69 syl 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> U. A C_ V )
71 67 70 sstrd 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( m u. n ) C_ V )
72 71 ssdifssd 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( ( m u. n ) \ { x } ) C_ V )
73 1 8 3 lspcl 
 |-  ( ( W e. LMod /\ ( ( m u. n ) \ { x } ) C_ V ) -> ( N ` ( ( m u. n ) \ { x } ) ) e. P )
74 65 72 73 syl2anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( N ` ( ( m u. n ) \ { x } ) ) e. P )
75 simp1r 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> r e. ( Base ` ( Scalar ` W ) ) )
76 ssun1 
 |-  m C_ ( m u. n )
77 ssdif 
 |-  ( m C_ ( m u. n ) -> ( m \ { x } ) C_ ( ( m u. n ) \ { x } ) )
78 76 77 mp1i 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( m \ { x } ) C_ ( ( m u. n ) \ { x } ) )
79 1 3 lspss 
 |-  ( ( W e. LMod /\ ( ( m u. n ) \ { x } ) C_ V /\ ( m \ { x } ) C_ ( ( m u. n ) \ { x } ) ) -> ( N ` ( m \ { x } ) ) C_ ( N ` ( ( m u. n ) \ { x } ) ) )
80 65 72 78 79 syl3anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( N ` ( m \ { x } ) ) C_ ( N ` ( ( m u. n ) \ { x } ) ) )
81 simp3l 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> v e. ( N ` ( m \ { x } ) ) )
82 80 81 sseldd 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> v e. ( N ` ( ( m u. n ) \ { x } ) ) )
83 ssun2 
 |-  n C_ ( m u. n )
84 ssdif 
 |-  ( n C_ ( m u. n ) -> ( n \ { x } ) C_ ( ( m u. n ) \ { x } ) )
85 83 84 mp1i 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( n \ { x } ) C_ ( ( m u. n ) \ { x } ) )
86 1 3 lspss 
 |-  ( ( W e. LMod /\ ( ( m u. n ) \ { x } ) C_ V /\ ( n \ { x } ) C_ ( ( m u. n ) \ { x } ) ) -> ( N ` ( n \ { x } ) ) C_ ( N ` ( ( m u. n ) \ { x } ) ) )
87 65 72 85 86 syl3anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( N ` ( n \ { x } ) ) C_ ( N ` ( ( m u. n ) \ { x } ) ) )
88 simp3r 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> w e. ( N ` ( n \ { x } ) ) )
89 87 88 sseldd 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> w e. ( N ` ( ( m u. n ) \ { x } ) ) )
90 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
91 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
92 eqid 
 |-  ( +g ` W ) = ( +g ` W )
93 eqid 
 |-  ( .s ` W ) = ( .s ` W )
94 90 91 92 93 8 lsscl 
 |-  ( ( ( N ` ( ( m u. n ) \ { x } ) ) e. P /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ v e. ( N ` ( ( m u. n ) \ { x } ) ) /\ w e. ( N ` ( ( m u. n ) \ { x } ) ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. ( N ` ( ( m u. n ) \ { x } ) ) )
95 74 75 82 89 94 syl13anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. ( N ` ( ( m u. n ) \ { x } ) ) )
96 difeq1 
 |-  ( u = ( m u. n ) -> ( u \ { x } ) = ( ( m u. n ) \ { x } ) )
97 96 fveq2d 
 |-  ( u = ( m u. n ) -> ( N ` ( u \ { x } ) ) = ( N ` ( ( m u. n ) \ { x } ) ) )
98 97 eliuni 
 |-  ( ( ( m u. n ) e. A /\ ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. ( N ` ( ( m u. n ) \ { x } ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. U_ u e. A ( N ` ( u \ { x } ) ) )
99 64 95 98 syl2anc 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. U_ u e. A ( N ` ( u \ { x } ) ) )
100 99 12 eleqtrrdi 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) /\ ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T )
101 100 3expia 
 |-  ( ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) /\ ( m e. A /\ n e. A ) ) -> ( ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T ) )
102 101 rexlimdvva 
 |-  ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) -> ( E. m e. A E. n e. A ( v e. ( N ` ( m \ { x } ) ) /\ w e. ( N ` ( n \ { x } ) ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T ) )
103 59 102 biimtrid 
 |-  ( ( ph /\ r e. ( Base ` ( Scalar ` W ) ) ) -> ( ( v e. T /\ w e. T ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T ) )
104 103 exp4b 
 |-  ( ph -> ( r e. ( Base ` ( Scalar ` W ) ) -> ( v e. T -> ( w e. T -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T ) ) ) )
105 104 3imp2 
 |-  ( ( ph /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ v e. T /\ w e. T ) ) -> ( ( r ( .s ` W ) v ) ( +g ` W ) w ) e. T )
106 13 14 15 16 17 18 31 42 105 islssd 
 |-  ( ph -> T e. P )
107 eldifi 
 |-  ( y e. ( U. A \ { x } ) -> y e. U. A )
108 107 adantl 
 |-  ( ( ph /\ y e. ( U. A \ { x } ) ) -> y e. U. A )
109 eldifn 
 |-  ( y e. ( U. A \ { x } ) -> -. y e. { x } )
110 109 ad2antlr 
 |-  ( ( ( ph /\ y e. ( U. A \ { x } ) ) /\ u e. A ) -> -. y e. { x } )
111 eldif 
 |-  ( y e. ( u \ { x } ) <-> ( y e. u /\ -. y e. { x } ) )
112 1 3 lspssid 
 |-  ( ( W e. LMod /\ ( u \ { x } ) C_ V ) -> ( u \ { x } ) C_ ( N ` ( u \ { x } ) ) )
113 20 25 112 syl2an2r 
 |-  ( ( ph /\ u e. A ) -> ( u \ { x } ) C_ ( N ` ( u \ { x } ) ) )
114 113 adantlr 
 |-  ( ( ( ph /\ y e. ( U. A \ { x } ) ) /\ u e. A ) -> ( u \ { x } ) C_ ( N ` ( u \ { x } ) ) )
115 114 sseld 
 |-  ( ( ( ph /\ y e. ( U. A \ { x } ) ) /\ u e. A ) -> ( y e. ( u \ { x } ) -> y e. ( N ` ( u \ { x } ) ) ) )
116 111 115 biimtrrid 
 |-  ( ( ( ph /\ y e. ( U. A \ { x } ) ) /\ u e. A ) -> ( ( y e. u /\ -. y e. { x } ) -> y e. ( N ` ( u \ { x } ) ) ) )
117 110 116 mpan2d 
 |-  ( ( ( ph /\ y e. ( U. A \ { x } ) ) /\ u e. A ) -> ( y e. u -> y e. ( N ` ( u \ { x } ) ) ) )
118 117 reximdva 
 |-  ( ( ph /\ y e. ( U. A \ { x } ) ) -> ( E. u e. A y e. u -> E. u e. A y e. ( N ` ( u \ { x } ) ) ) )
119 eluni2 
 |-  ( y e. U. A <-> E. u e. A y e. u )
120 eliun 
 |-  ( y e. U_ u e. A ( N ` ( u \ { x } ) ) <-> E. u e. A y e. ( N ` ( u \ { x } ) ) )
121 118 119 120 3imtr4g 
 |-  ( ( ph /\ y e. ( U. A \ { x } ) ) -> ( y e. U. A -> y e. U_ u e. A ( N ` ( u \ { x } ) ) ) )
122 108 121 mpd 
 |-  ( ( ph /\ y e. ( U. A \ { x } ) ) -> y e. U_ u e. A ( N ` ( u \ { x } ) ) )
123 122 ex 
 |-  ( ph -> ( y e. ( U. A \ { x } ) -> y e. U_ u e. A ( N ` ( u \ { x } ) ) ) )
124 123 ssrdv 
 |-  ( ph -> ( U. A \ { x } ) C_ U_ u e. A ( N ` ( u \ { x } ) ) )
125 124 12 sseqtrrdi 
 |-  ( ph -> ( U. A \ { x } ) C_ T )
126 106 125 jca 
 |-  ( ph -> ( T e. P /\ ( U. A \ { x } ) C_ T ) )