exsslsb - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > exsslsb		Structured version Visualization version GIF version

Theorem exsslsb 34222

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

**Hypotheses**
Ref	Expression
exsslsb.b	⊢ 𝐵 = (Base‘𝑊)
exsslsb.j	⊢ 𝐽 = (LBasis‘𝑊)
exsslsb.k	⊢ 𝐾 = (LSpan‘𝑊)
exsslsb.w	⊢ (𝜑 → 𝑊 ∈ LVec)
exsslsb.s	⊢ (𝜑 → 𝑆 ∈ Fin)
exsslsb.1	⊢ (𝜑 → 𝑆 ⊆ 𝐵)
exsslsb.2	⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)

**Assertion**
Ref	Expression
exsslsb	⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)

Distinct variable groups: 𝐵,𝑠 𝐽,𝑠 𝐾,𝑠 𝑆,𝑠 𝜑,𝑠 Allowed substitution hint: 𝑊(𝑠)

Proof of Theorem exsslsb Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1947	. 2 ⊢ Ⅎ𝑠𝜑
2		exsslsb.w	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LVec)
3	2	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑊 ∈ LVec)
4		simplr 781	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
5	4	elin2d 4151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
6	5	elin1d 4150	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝒫 𝑆)
7	6	elpwid 4566	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝑆)
8		exsslsb.1	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
9	8	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑆 ⊆ 𝐵)
10	7, 9	sstrd 3941	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝐵)
11		lveclmod 21374	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
12		exsslsb.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
13		eqid 2761	. . . . . . . 8 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
14		exsslsb.k	. . . . . . . 8 ⊢ 𝐾 = (LSpan‘𝑊)
15	12, 13, 14	lspf 21242	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
16	2, 11, 15	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
17	16	ffnd 6708	. . . . 5 ⊢ (𝜑 → 𝐾 Fn 𝒫 𝐵)
18	17	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝐾 Fn 𝒫 𝐵)
19	5	elin2d 4151	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (^◡𝐾 “ {𝐵}))
20		fniniseg 7057	. . . . 5 ⊢ (𝐾 Fn 𝒫 𝐵 → (𝑠 ∈ (^◡𝐾 “ {𝐵}) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ (𝐾‘𝑠) = 𝐵)))
21	20	simplbda 505	. . . 4 ⊢ ((𝐾 Fn 𝒫 𝐵 ∧ 𝑠 ∈ (^◡𝐾 “ {𝐵})) → (𝐾‘𝑠) = 𝐵)
22	18, 19, 21	syl2anc 596	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝐾‘𝑠) = 𝐵)
23	2, 11	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ LMod)
24	23	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑊 ∈ LMod)
25		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊊ 𝑠)
26	25	pssssd 4048	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑠)
27	7	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ⊆ 𝑆)
28	26, 27	sstrd 3941	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑆)
29	9	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ⊆ 𝐵)
30	28, 29	sstrd 3941	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝐵)
31	12, 14	lspssv 21251	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵) → (𝐾‘𝑢) ⊆ 𝐵)
32	24, 30, 31	syl2anc 596	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊆ 𝐵)
33		hashf 14475	. . . . . . . . . . . 12 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
34		ffun 6710	. . . . . . . . . . . 12 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
35	33, 34	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ♯)
36		exsslsb.s	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ Fin)
37		pwssfi 9185	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ Fin → (𝑆 ∈ Fin ↔ 𝒫 𝑆 ⊆ Fin))
38	37	ibi 270	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → 𝒫 𝑆 ⊆ Fin)
39	36, 38	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝒫 𝑆 ⊆ Fin)
40	39	ssinss1d 4193	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})) ⊆ Fin)
41	40	sselda 3931	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → 𝑠 ∈ Fin)
42		hashcl 14493	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
43	41, 42	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ ℕ₀)
44		nn0uz 12996	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
45	43, 44	eleqtrdi 2871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ (ℤ_≥‘0))
46	1, 35, 45	funimassd 6949	. . . . . . . . . 10 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
47	46	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
48	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ♯:V⟶(ℕ₀ ∪ {+∞}))
49	48	ffnd 6708	. . . . . . . . . . . 12 ⊢ (𝜑 → ♯ Fn V)
50	49	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ♯ Fn V)
51	50	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ♯ Fn V)
52		vex 3455	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ V)
54	36	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ∈ Fin)
55	54, 28	sselpwd 5290	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝑆)
56	55	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝑆)
57	18	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝐾 Fn 𝒫 𝐵)
58	12	fvexi 6897	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝐵 ∈ V)
60	59, 30	sselpwd 5290	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝐵)
61	60	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝐵)
62		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) = 𝐵)
63		fvex 6896	. . . . . . . . . . . . . 14 ⊢ (𝐾‘𝑢) ∈ V
64	63	elsn 4599	. . . . . . . . . . . . 13 ⊢ ((𝐾‘𝑢) ∈ {𝐵} ↔ (𝐾‘𝑢) = 𝐵)
65	62, 64	sylibr 237	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) ∈ {𝐵})
66	57, 61, 65	elpreimad 7056	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (^◡𝐾 “ {𝐵}))
67	56, 66	elind 4146	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
68	51, 53, 67	fnfvimad 7238	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
69		infssuzle 13051	. . . . . . . . 9 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
70	47, 68, 69	syl2an2r 698	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
71	54, 27	ssfid 9253	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ∈ Fin)
72	71	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑠 ∈ Fin)
73		simplr 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊊ 𝑠)
74		hashpss 14547	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠) → (♯‘𝑢) < (♯‘𝑠))
75	72, 73, 74	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < (♯‘𝑠))
76		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
77	75, 76	breqtrd 5131	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
78	26	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊆ 𝑠)
79	72, 78	ssfid 9253	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ Fin)
80		hashcl 14493	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
81	79, 80	syl 18	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℕ₀)
82	81	nn0red 12661	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℝ)
83	72, 42	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℕ₀)
84	83	nn0red 12661	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℝ)
85	76, 84	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ ℝ)
86	82, 85	ltnled 11450	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ((♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ↔ ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢)))
87	77, 86	mpbid 235	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
88	70, 87	pm2.65da 829	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ¬ (𝐾‘𝑢) = 𝐵)
89	88	neqned 2963	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ≠ 𝐵)
90		df-pss 3919	. . . . . 6 ⊢ ((𝐾‘𝑢) ⊊ 𝐵 ↔ ((𝐾‘𝑢) ⊆ 𝐵 ∧ (𝐾‘𝑢) ≠ 𝐵))
91	32, 89, 90	sylanbrc 595	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊊ 𝐵)
92	91	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
93	92	alrimiv 1960	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
94		exsslsb.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
95	12, 94, 14	islbs3 21426	. . . 4 ⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))))
96	95	biimpar 483	. . 3 ⊢ ((𝑊 ∈ LVec ∧ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))) → 𝑠 ∈ 𝐽)
97	3, 10, 22, 93, 96	syl13anc 1399	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝐽)
98	36	elexd 3474	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
99		pwidg 4577	. . . . . . . 8 ⊢ (𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆)
100	36, 99	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑆)
101	36, 8	elpwd 4563	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)
102		exsslsb.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)
103		fvex 6896	. . . . . . . . . 10 ⊢ (𝐾‘𝑆) ∈ V
104	103	elsn 4599	. . . . . . . . 9 ⊢ ((𝐾‘𝑆) ∈ {𝐵} ↔ (𝐾‘𝑆) = 𝐵)
105	102, 104	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘𝑆) ∈ {𝐵})
106	17, 101, 105	elpreimad 7056	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (^◡𝐾 “ {𝐵}))
107	100, 106	elind 4146	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
108	49, 98, 107	fnfvimad 7238	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
109	108	ne0d 4288	. . . 4 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅)
110		infssuzcl 13052	. . . 4 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
111	46, 109, 110	syl2anc 596	. . 3 ⊢ (𝜑 → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
112		fvelima2 6935	. . 3 ⊢ ((♯ Fn V ∧ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
113	49, 111, 112	syl2anc 596	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
114	1, 97, 7, 113	reximd2a 3273	1 ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∃wrex 3087 Vcvv 3451 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ⊊ wpss 3900 ∅c0 4279 𝒫 cpw 4557 {csn 4584 class class class wbr 5103 ^◡ccnv 5650 “ cima 5654 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 Fincfn 8966 infcinf 9426 ℝcr 11192 0cc0 11193 +∞cpnf 11333 < clt 11336 ≤ cle 11337 ℕ₀cn0 12599 ℤ_≥cuz 12958 ♯chash 14467 Basecbs 17380 LModclmod 21128 LSubSpclss 21199 LSpanclspn 21239 LBasisclbs 21342 LVecclvec 21370

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-tpos 8236 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-oadd 8473 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-inf 9428 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-xnn0 12673 df-z 12687 df-uz 12959 df-fz 13633 df-hash 14468 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-0g 17605 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-grp 19140 df-minusg 19141 df-sbg 19142 df-cmn 19989 df-abl 19990 df-mgp 20354 df-rng 20368 df-ur 20401 df-ring 20454 df-oppr 20560 df-dvdsr 20580 df-unit 20581 df-invr 20611 df-drng 20975 df-lmod 21130 df-lss 21200 df-lsp 21240 df-lbs 21343 df-lvec 21371

This theorem is used by: lbslelsp 34223

W3C validator