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

Metamath Proof Explorer

Theorem exsslsb

Description: Any finite generating set S of a vector space W contains a basis. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses exsslsb.b 
|- B = ( Base ` W )
exsslsb.j 
|- J = ( LBasis ` W )
exsslsb.k 
|- K = ( LSpan ` W )
exsslsb.w 
|- ( ph -> W e. LVec )
exsslsb.s 
|- ( ph -> S e. Fin )
exsslsb.1 
|- ( ph -> S C_ B )
exsslsb.2 
|- ( ph -> ( K ` S ) = B )
Assertion exsslsb 
|- ( ph -> E. s e. J s C_ S )

Proof

Step Hyp Ref Expression
1 exsslsb.b 
 |-  B = ( Base ` W )
2 exsslsb.j 
 |-  J = ( LBasis ` W )
3 exsslsb.k 
 |-  K = ( LSpan ` W )
4 exsslsb.w 
 |-  ( ph -> W e. LVec )
5 exsslsb.s 
 |-  ( ph -> S e. Fin )
6 exsslsb.1 
 |-  ( ph -> S C_ B )
7 exsslsb.2 
 |-  ( ph -> ( K ` S ) = B )
8 nfv 
 |-  F/ s ph
9 4 ad2antrr 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> W e. LVec )
10 simplr 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) )
11 10 elin2d 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s e. ( ~P S i^i ( `' K " { B } ) ) )
12 11 elin1d 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s e. ~P S )
13 12 elpwid 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s C_ S )
14 6 ad2antrr 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> S C_ B )
15 13 14 sstrd 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s C_ B )
16 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
17 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
18 1 17 3 lspf 
 |-  ( W e. LMod -> K : ~P B --> ( LSubSp ` W ) )
19 4 16 18 3syl 
 |-  ( ph -> K : ~P B --> ( LSubSp ` W ) )
20 19 ffnd 
 |-  ( ph -> K Fn ~P B )
21 20 ad2antrr 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> K Fn ~P B )
22 11 elin2d 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s e. ( `' K " { B } ) )
23 fniniseg 
 |-  ( K Fn ~P B -> ( s e. ( `' K " { B } ) <-> ( s e. ~P B /\ ( K ` s ) = B ) ) )
24 23 simplbda 
 |-  ( ( K Fn ~P B /\ s e. ( `' K " { B } ) ) -> ( K ` s ) = B )
25 21 22 24 syl2anc 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> ( K ` s ) = B )
26 4 16 syl 
 |-  ( ph -> W e. LMod )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> W e. LMod )
28 simpr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u C. s )
29 28 pssssd 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u C_ s )
30 13 adantr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> s C_ S )
31 29 30 sstrd 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u C_ S )
32 14 adantr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> S C_ B )
33 31 32 sstrd 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u C_ B )
34 1 3 lspssv 
 |-  ( ( W e. LMod /\ u C_ B ) -> ( K ` u ) C_ B )
35 27 33 34 syl2anc 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> ( K ` u ) C_ B )
36 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
37 ffun 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> Fun # )
38 36 37 mp1i 
 |-  ( ph -> Fun # )
39 pwssfi 
 |-  ( S e. Fin -> ( S e. Fin <-> ~P S C_ Fin ) )
40 39 ibi 
 |-  ( S e. Fin -> ~P S C_ Fin )
41 5 40 syl 
 |-  ( ph -> ~P S C_ Fin )
42 41 ssinss1d 
 |-  ( ph -> ( ~P S i^i ( `' K " { B } ) ) C_ Fin )
43 42 sselda 
 |-  ( ( ph /\ s e. ( ~P S i^i ( `' K " { B } ) ) ) -> s e. Fin )
44 hashcl 
 |-  ( s e. Fin -> ( # ` s ) e. NN0 )
45 43 44 syl 
 |-  ( ( ph /\ s e. ( ~P S i^i ( `' K " { B } ) ) ) -> ( # ` s ) e. NN0 )
46 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
47 45 46 eleqtrdi 
 |-  ( ( ph /\ s e. ( ~P S i^i ( `' K " { B } ) ) ) -> ( # ` s ) e. ( ZZ>= ` 0 ) )
48 8 38 47 funimassd 
 |-  ( ph -> ( # " ( ~P S i^i ( `' K " { B } ) ) ) C_ ( ZZ>= ` 0 ) )
49 48 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> ( # " ( ~P S i^i ( `' K " { B } ) ) ) C_ ( ZZ>= ` 0 ) )
50 36 a1i 
 |-  ( ph -> # : _V --> ( NN0 u. { +oo } ) )
51 50 ffnd 
 |-  ( ph -> # Fn _V )
52 51 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> # Fn _V )
53 52 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> # Fn _V )
54 vex 
 |-  u e. _V
55 54 a1i 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. _V )
56 5 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> S e. Fin )
57 56 31 sselpwd 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u e. ~P S )
58 57 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. ~P S )
59 21 ad2antrr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> K Fn ~P B )
60 1 fvexi 
 |-  B e. _V
61 60 a1i 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> B e. _V )
62 61 33 sselpwd 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> u e. ~P B )
63 62 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. ~P B )
64 simpr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( K ` u ) = B )
65 fvex 
 |-  ( K ` u ) e. _V
66 65 elsn 
 |-  ( ( K ` u ) e. { B } <-> ( K ` u ) = B )
67 64 66 sylibr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( K ` u ) e. { B } )
68 59 63 67 elpreimad 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. ( `' K " { B } ) )
69 58 68 elind 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. ( ~P S i^i ( `' K " { B } ) ) )
70 53 55 69 fnfvimad 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` u ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) )
71 infssuzle 
 |-  ( ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) C_ ( ZZ>= ` 0 ) /\ ( # ` u ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) ) -> inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) <_ ( # ` u ) )
72 49 70 71 syl2an2r 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) <_ ( # ` u ) )
73 56 30 ssfid 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> s e. Fin )
74 73 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> s e. Fin )
75 simplr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u C. s )
76 hashpss 
 |-  ( ( s e. Fin /\ u C. s ) -> ( # ` u ) < ( # ` s ) )
77 74 75 76 syl2anc 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` u ) < ( # ` s ) )
78 simpllr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) )
79 77 78 breqtrd 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` u ) < inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) )
80 29 adantr 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u C_ s )
81 74 80 ssfid 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> u e. Fin )
82 hashcl 
 |-  ( u e. Fin -> ( # ` u ) e. NN0 )
83 81 82 syl 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` u ) e. NN0 )
84 83 nn0red 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` u ) e. RR )
85 74 44 syl 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` s ) e. NN0 )
86 85 nn0red 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( # ` s ) e. RR )
87 78 86 eqeltrrd 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) e. RR )
88 84 87 ltnled 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> ( ( # ` u ) < inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) <-> -. inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) <_ ( # ` u ) ) )
89 79 88 mpbid 
 |-  ( ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) /\ ( K ` u ) = B ) -> -. inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) <_ ( # ` u ) )
90 72 89 pm2.65da 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> -. ( K ` u ) = B )
91 90 neqned 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> ( K ` u ) =/= B )
92 df-pss 
 |-  ( ( K ` u ) C. B <-> ( ( K ` u ) C_ B /\ ( K ` u ) =/= B ) )
93 35 91 92 sylanbrc 
 |-  ( ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) /\ u C. s ) -> ( K ` u ) C. B )
94 93 ex 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> ( u C. s -> ( K ` u ) C. B ) )
95 94 alrimiv 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> A. u ( u C. s -> ( K ` u ) C. B ) )
96 1 2 3 islbs3 
 |-  ( W e. LVec -> ( s e. J <-> ( s C_ B /\ ( K ` s ) = B /\ A. u ( u C. s -> ( K ` u ) C. B ) ) ) )
97 96 biimpar 
 |-  ( ( W e. LVec /\ ( s C_ B /\ ( K ` s ) = B /\ A. u ( u C. s -> ( K ` u ) C. B ) ) ) -> s e. J )
98 9 15 25 95 97 syl13anc 
 |-  ( ( ( ph /\ s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ) /\ ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) ) -> s e. J )
99 5 elexd 
 |-  ( ph -> S e. _V )
100 pwidg 
 |-  ( S e. Fin -> S e. ~P S )
101 5 100 syl 
 |-  ( ph -> S e. ~P S )
102 5 6 elpwd 
 |-  ( ph -> S e. ~P B )
103 fvex 
 |-  ( K ` S ) e. _V
104 103 elsn 
 |-  ( ( K ` S ) e. { B } <-> ( K ` S ) = B )
105 7 104 sylibr 
 |-  ( ph -> ( K ` S ) e. { B } )
106 20 102 105 elpreimad 
 |-  ( ph -> S e. ( `' K " { B } ) )
107 101 106 elind 
 |-  ( ph -> S e. ( ~P S i^i ( `' K " { B } ) ) )
108 51 99 107 fnfvimad 
 |-  ( ph -> ( # ` S ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) )
109 108 ne0d 
 |-  ( ph -> ( # " ( ~P S i^i ( `' K " { B } ) ) ) =/= (/) )
110 infssuzcl 
 |-  ( ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) C_ ( ZZ>= ` 0 ) /\ ( # " ( ~P S i^i ( `' K " { B } ) ) ) =/= (/) ) -> inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) )
111 48 109 110 syl2anc 
 |-  ( ph -> inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) )
112 fvelima2 
 |-  ( ( # Fn _V /\ inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) e. ( # " ( ~P S i^i ( `' K " { B } ) ) ) ) -> E. s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) )
113 51 111 112 syl2anc 
 |-  ( ph -> E. s e. ( _V i^i ( ~P S i^i ( `' K " { B } ) ) ) ( # ` s ) = inf ( ( # " ( ~P S i^i ( `' K " { B } ) ) ) , RR , < ) )
114 8 98 13 113 reximd2a 
 |-  ( ph -> E. s e. J s C_ S )