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 33987

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 1944	. 2 ⊢ Ⅎ𝑠𝜑
2		exsslsb.w	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LVec)
3	2	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑊 ∈ LVec)
4		simplr 780	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
5	4	elin2d 4158	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
6	5	elin1d 4157	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝒫 𝑆)
7	6	elpwid 4571	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝑆)
8		exsslsb.1	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
9	8	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑆 ⊆ 𝐵)
10	7, 9	sstrd 3947	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝐵)
11		lveclmod 21227	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
12		exsslsb.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
13		eqid 2763	. . . . . . . 8 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
14		exsslsb.k	. . . . . . . 8 ⊢ 𝐾 = (LSpan‘𝑊)
15	12, 13, 14	lspf 21095	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
16	2, 11, 15	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
17	16	ffnd 6706	. . . . 5 ⊢ (𝜑 → 𝐾 Fn 𝒫 𝐵)
18	17	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝐾 Fn 𝒫 𝐵)
19	5	elin2d 4158	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (^◡𝐾 “ {𝐵}))
20		fniniseg 7055	. . . . 5 ⊢ (𝐾 Fn 𝒫 𝐵 → (𝑠 ∈ (^◡𝐾 “ {𝐵}) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ (𝐾‘𝑠) = 𝐵)))
21	20	simplbda 504	. . . 4 ⊢ ((𝐾 Fn 𝒫 𝐵 ∧ 𝑠 ∈ (^◡𝐾 “ {𝐵})) → (𝐾‘𝑠) = 𝐵)
22	18, 19, 21	syl2anc 595	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝐾‘𝑠) = 𝐵)
23	2, 11	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ LMod)
24	23	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑊 ∈ LMod)
25		simpr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊊ 𝑠)
26	25	pssssd 4054	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑠)
27	7	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ⊆ 𝑆)
28	26, 27	sstrd 3947	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑆)
29	9	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ⊆ 𝐵)
30	28, 29	sstrd 3947	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝐵)
31	12, 14	lspssv 21104	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵) → (𝐾‘𝑢) ⊆ 𝐵)
32	24, 30, 31	syl2anc 595	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊆ 𝐵)
33		hashf 14370	. . . . . . . . . . . 12 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
34		ffun 6708	. . . . . . . . . . . 12 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
35	33, 34	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ♯)
36		exsslsb.s	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ Fin)
37		pwssfi 9157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ Fin → (𝑆 ∈ Fin ↔ 𝒫 𝑆 ⊆ Fin))
38	37	ibi 270	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → 𝒫 𝑆 ⊆ Fin)
39	36, 38	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝒫 𝑆 ⊆ Fin)
40	39	ssinss1d 4200	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})) ⊆ Fin)
41	40	sselda 3937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → 𝑠 ∈ Fin)
42		hashcl 14388	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
43	41, 42	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ ℕ₀)
44		nn0uz 12895	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
45	43, 44	eleqtrdi 2873	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ (ℤ_≥‘0))
46	1, 35, 45	funimassd 6947	. . . . . . . . . 10 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
47	46	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
48	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ♯:V⟶(ℕ₀ ∪ {+∞}))
49	48	ffnd 6706	. . . . . . . . . . . 12 ⊢ (𝜑 → ♯ Fn V)
50	49	ad3antrrr 742	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ♯ Fn V)
51	50	adantr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ♯ Fn V)
52		vex 3459	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ V)
54	36	ad3antrrr 742	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ∈ Fin)
55	54, 28	sselpwd 5299	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝑆)
56	55	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝑆)
57	18	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝐾 Fn 𝒫 𝐵)
58	12	fvexi 6895	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝐵 ∈ V)
60	59, 30	sselpwd 5299	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝐵)
61	60	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝐵)
62		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) = 𝐵)
63		fvex 6894	. . . . . . . . . . . . . 14 ⊢ (𝐾‘𝑢) ∈ V
64	63	elsn 4604	. . . . . . . . . . . . 13 ⊢ ((𝐾‘𝑢) ∈ {𝐵} ↔ (𝐾‘𝑢) = 𝐵)
65	62, 64	sylibr 237	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) ∈ {𝐵})
66	57, 61, 65	elpreimad 7054	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (^◡𝐾 “ {𝐵}))
67	56, 66	elind 4153	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
68	51, 53, 67	fnfvimad 7232	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
69		infssuzle 12950	. . . . . . . . 9 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
70	47, 68, 69	syl2an2r 697	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
71	54, 27	ssfid 9225	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ∈ Fin)
72	71	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑠 ∈ Fin)
73		simplr 780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊊ 𝑠)
74		hashpss 14442	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠) → (♯‘𝑢) < (♯‘𝑠))
75	72, 73, 74	syl2anc 595	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < (♯‘𝑠))
76		simpllr 787	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
77	75, 76	breqtrd 5137	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
78	26	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊆ 𝑠)
79	72, 78	ssfid 9225	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ Fin)
80		hashcl 14388	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
81	79, 80	syl 18	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℕ₀)
82	81	nn0red 12561	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℝ)
83	72, 42	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℕ₀)
84	83	nn0red 12561	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℝ)
85	76, 84	eqeltrrd 2864	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ ℝ)
86	82, 85	ltnled 11352	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ((♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ↔ ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢)))
87	77, 86	mpbid 235	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
88	70, 87	pm2.65da 828	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ¬ (𝐾‘𝑢) = 𝐵)
89	88	neqned 2965	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ≠ 𝐵)
90		df-pss 3925	. . . . . 6 ⊢ ((𝐾‘𝑢) ⊊ 𝐵 ↔ ((𝐾‘𝑢) ⊆ 𝐵 ∧ (𝐾‘𝑢) ≠ 𝐵))
91	32, 89, 90	sylanbrc 594	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊊ 𝐵)
92	91	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
93	92	alrimiv 1957	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
94		exsslsb.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
95	12, 94, 14	islbs3 21279	. . . 4 ⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))))
96	95	biimpar 482	. . 3 ⊢ ((𝑊 ∈ LVec ∧ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))) → 𝑠 ∈ 𝐽)
97	3, 10, 22, 93, 96	syl13anc 1399	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝐽)
98	36	elexd 3478	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
99		pwidg 4582	. . . . . . . 8 ⊢ (𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆)
100	36, 99	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑆)
101	36, 8	elpwd 4568	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)
102		exsslsb.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)
103		fvex 6894	. . . . . . . . . 10 ⊢ (𝐾‘𝑆) ∈ V
104	103	elsn 4604	. . . . . . . . 9 ⊢ ((𝐾‘𝑆) ∈ {𝐵} ↔ (𝐾‘𝑆) = 𝐵)
105	102, 104	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘𝑆) ∈ {𝐵})
106	17, 101, 105	elpreimad 7054	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (^◡𝐾 “ {𝐵}))
107	100, 106	elind 4153	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
108	49, 98, 107	fnfvimad 7232	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
109	108	ne0d 4295	. . . 4 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅)
110		infssuzcl 12951	. . . 4 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
111	46, 109, 110	syl2anc 595	. . 3 ⊢ (𝜑 → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
112		fvelima2 6933	. . 3 ⊢ ((♯ Fn V ∧ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
113	49, 111, 112	syl2anc 595	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
114	1, 97, 7, 113	reximd2a 3275	1 ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∃wrex 3089 Vcvv 3455 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ⊊ wpss 3906 ∅c0 4286 𝒫 cpw 4562 {csn 4589 class class class wbr 5109 ^◡ccnv 5660 “ cima 5664 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 Fincfn 8939 infcinf 9397 ℝcr 11094 0cc0 11095 +∞cpnf 11235 < clt 11238 ≤ cle 11239 ℕ₀cn0 12499 ℤ_≥cuz 12857 ♯chash 14362 Basecbs 17264 LModclmod 20981 LSubSpclss 21052 LSpanclspn 21092 LBasisclbs 21195 LVecclvec 21223

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-tpos 8218 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9398 df-inf 9399 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-fz 13531 df-hash 14363 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-0g 17489 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-grp 18998 df-minusg 18999 df-sbg 19000 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-invr 20466 df-drng 20829 df-lmod 20983 df-lss 21053 df-lsp 21093 df-lbs 21196 df-lvec 21224

This theorem is referenced by: lbslelsp 33988

W3C validator