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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
exsslsb.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
exsslsb.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
exsslsb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
exsslsb.s ⊢ ( 𝜑 → 𝑆 ∈ Fin )
exsslsb.1 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
exsslsb.2 ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) = 𝐵 )
Assertion exsslsb ( 𝜑 → ∃ 𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 exsslsb.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 exsslsb.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 exsslsb.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
4 exsslsb.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 exsslsb.s ⊢ ( 𝜑 → 𝑆 ∈ Fin )
6 exsslsb.1 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
7 exsslsb.2 ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) = 𝐵 )
8 nfv ⊢ Ⅎ 𝑠 𝜑
9 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑊 ∈ LVec )
10 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) )
11 10 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) )
12 11 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ∈ 𝒫 𝑆 )
13 12 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ⊆ 𝑆 )
14 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑆 ⊆ 𝐵 )
15 13 14 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ⊆ 𝐵 )
16 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
17 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
18 1 17 3 lspf ⊢ ( 𝑊 ∈ LMod → 𝐾 : 𝒫 𝐵 ⟶ ( LSubSp ‘ 𝑊 ) )
19 4 16 18 3syl ⊢ ( 𝜑 → 𝐾 : 𝒫 𝐵 ⟶ ( LSubSp ‘ 𝑊 ) )
20 19 ffnd ⊢ ( 𝜑 → 𝐾 Fn 𝒫 𝐵 )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝐾 Fn 𝒫 𝐵 )
22 11 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ∈ ( ◡ 𝐾 “ { 𝐵 } ) )
23 fniniseg ⊢ ( 𝐾 Fn 𝒫 𝐵 → ( 𝑠 ∈ ( ◡ 𝐾 “ { 𝐵 } ) ↔ ( 𝑠 ∈ 𝒫 𝐵 ∧ ( 𝐾 ‘ 𝑠 ) = 𝐵 ) ) )
24 23 simplbda ⊢ ( ( 𝐾 Fn 𝒫 𝐵 ∧ 𝑠 ∈ ( ◡ 𝐾 “ { 𝐵 } ) ) → ( 𝐾 ‘ 𝑠 ) = 𝐵 )
25 21 22 24 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → ( 𝐾 ‘ 𝑠 ) = 𝐵 )
26 4 16 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
27 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑊 ∈ LMod )
28 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ⊊ 𝑠 )
29 28 pssssd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ⊆ 𝑠 )
30 13 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑠 ⊆ 𝑆 )
31 29 30 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ⊆ 𝑆 )
32 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑆 ⊆ 𝐵 )
33 31 32 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ⊆ 𝐵 )
34 1 3 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑢 ) ⊆ 𝐵 )
35 27 33 34 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ( 𝐾 ‘ 𝑢 ) ⊆ 𝐵 )
36 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
37 ffun ⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → Fun ♯ )
38 36 37 mp1i ⊢ ( 𝜑 → Fun ♯ )
39 pwssfi ⊢ ( 𝑆 ∈ Fin → ( 𝑆 ∈ Fin ↔ 𝒫 𝑆 ⊆ Fin ) )
40 39 ibi ⊢ ( 𝑆 ∈ Fin → 𝒫 𝑆 ⊆ Fin )
41 5 40 syl ⊢ ( 𝜑 → 𝒫 𝑆 ⊆ Fin )
42 41 ssinss1d ⊢ ( 𝜑 → ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ⊆ Fin )
43 42 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) → 𝑠 ∈ Fin )
44 hashcl ⊢ ( 𝑠 ∈ Fin → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
46 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
47 45 46 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) → ( ♯ ‘ 𝑠 ) ∈ ( ℤ≥ ‘ 0 ) )
48 8 38 47 funimassd ⊢ ( 𝜑 → ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ⊆ ( ℤ≥ ‘ 0 ) )
49 48 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ⊆ ( ℤ≥ ‘ 0 ) )
50 36 a1i ⊢ ( 𝜑 → ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) )
51 50 ffnd ⊢ ( 𝜑 → ♯ Fn V )
52 51 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ♯ Fn V )
53 52 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ♯ Fn V )
54 vex ⊢ 𝑢 ∈ V
55 54 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ V )
56 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑆 ∈ Fin )
57 56 31 sselpwd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ∈ 𝒫 𝑆 )
58 57 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ 𝒫 𝑆 )
59 21 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝐾 Fn 𝒫 𝐵 )
60 1 fvexi ⊢ 𝐵 ∈ V
61 60 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝐵 ∈ V )
62 61 33 sselpwd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑢 ∈ 𝒫 𝐵 )
63 62 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ 𝒫 𝐵 )
64 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( 𝐾 ‘ 𝑢 ) = 𝐵 )
65 fvex ⊢ ( 𝐾 ‘ 𝑢 ) ∈ V
66 65 elsn ⊢ ( ( 𝐾 ‘ 𝑢 ) ∈ { 𝐵 } ↔ ( 𝐾 ‘ 𝑢 ) = 𝐵 )
67 64 66 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( 𝐾 ‘ 𝑢 ) ∈ { 𝐵 } )
68 59 63 67 elpreimad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ ( ◡ 𝐾 “ { 𝐵 } ) )
69 58 68 elind ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) )
70 53 55 69 fnfvimad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑢 ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) )
71 infssuzle ⊢ ( ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ⊆ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑢 ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) → inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ≤ ( ♯ ‘ 𝑢 ) )
72 49 70 71 syl2an2r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ≤ ( ♯ ‘ 𝑢 ) )
73 56 30 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → 𝑠 ∈ Fin )
74 73 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑠 ∈ Fin )
75 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ⊊ 𝑠 )
76 hashpss ⊢ ( ( 𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠 ) → ( ♯ ‘ 𝑢 ) < ( ♯ ‘ 𝑠 ) )
77 74 75 76 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑢 ) < ( ♯ ‘ 𝑠 ) )
78 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) )
79 77 78 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑢 ) < inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) )
80 29 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ⊆ 𝑠 )
81 74 80 ssfid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → 𝑢 ∈ Fin )
82 hashcl ⊢ ( 𝑢 ∈ Fin → ( ♯ ‘ 𝑢 ) ∈ ℕ0 )
83 81 82 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑢 ) ∈ ℕ0 )
84 83 nn0red ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑢 ) ∈ ℝ )
85 74 44 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
86 85 nn0red ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ♯ ‘ 𝑠 ) ∈ ℝ )
87 78 86 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ∈ ℝ )
88 84 87 ltnled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ( ( ♯ ‘ 𝑢 ) < inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ↔ ¬ inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ≤ ( ♯ ‘ 𝑢 ) ) )
89 79 88 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) ∧ ( 𝐾 ‘ 𝑢 ) = 𝐵 ) → ¬ inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ≤ ( ♯ ‘ 𝑢 ) )
90 72 89 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ¬ ( 𝐾 ‘ 𝑢 ) = 𝐵 )
91 90 neqned ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ( 𝐾 ‘ 𝑢 ) ≠ 𝐵 )
92 df-pss ⊢ ( ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 ↔ ( ( 𝐾 ‘ 𝑢 ) ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑢 ) ≠ 𝐵 ) )
93 35 91 92 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) ∧ 𝑢 ⊊ 𝑠 ) → ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 )
94 93 ex ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → ( 𝑢 ⊊ 𝑠 → ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 ) )
95 94 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → ∀ 𝑢 ( 𝑢 ⊊ 𝑠 → ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 ) )
96 1 2 3 islbs3 ⊢ ( 𝑊 ∈ LVec → ( 𝑠 ∈ 𝐽 ↔ ( 𝑠 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑠 ) = 𝐵 ∧ ∀ 𝑢 ( 𝑢 ⊊ 𝑠 → ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 ) ) ) )
97 96 biimpar ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑠 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑠 ) = 𝐵 ∧ ∀ 𝑢 ( 𝑢 ⊊ 𝑠 → ( 𝐾 ‘ 𝑢 ) ⊊ 𝐵 ) ) ) → 𝑠 ∈ 𝐽 )
98 9 15 25 95 97 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) ∧ ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ) → 𝑠 ∈ 𝐽 )
99 5 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
100 pwidg ⊢ ( 𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆 )
101 5 100 syl ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝑆 )
102 5 6 elpwd ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
103 fvex ⊢ ( 𝐾 ‘ 𝑆 ) ∈ V
104 103 elsn ⊢ ( ( 𝐾 ‘ 𝑆 ) ∈ { 𝐵 } ↔ ( 𝐾 ‘ 𝑆 ) = 𝐵 )
105 7 104 sylibr ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑆 ) ∈ { 𝐵 } )
106 20 102 105 elpreimad ⊢ ( 𝜑 → 𝑆 ∈ ( ◡ 𝐾 “ { 𝐵 } ) )
107 101 106 elind ⊢ ( 𝜑 → 𝑆 ∈ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) )
108 51 99 107 fnfvimad ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) )
109 108 ne0d ⊢ ( 𝜑 → ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ≠ ∅ )
110 infssuzcl ⊢ ( ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ⊆ ( ℤ≥ ‘ 0 ) ∧ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ≠ ∅ ) → inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) )
111 48 109 110 syl2anc ⊢ ( 𝜑 → inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) )
112 fvelima2 ⊢ ( ( ♯ Fn V ∧ inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) ∈ ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ) → ∃ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) )
113 51 111 112 syl2anc ⊢ ( 𝜑 → ∃ 𝑠 ∈ ( V ∩ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) ( ♯ ‘ 𝑠 ) = inf ( ( ♯ “ ( 𝒫 𝑆 ∩ ( ◡ 𝐾 “ { 𝐵 } ) ) ) , ℝ , < ) )
114 8 98 13 113 reximd2a ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆 )