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 33565

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 1914	. 2 ⊢ Ⅎ𝑠𝜑
2		exsslsb.w	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LVec)
3	2	ad2antrr 726	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑊 ∈ LVec)
4		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
5	4	elin2d 4164	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
6	5	elin1d 4163	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝒫 𝑆)
7	6	elpwid 4568	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝑆)
8		exsslsb.1	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
9	8	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑆 ⊆ 𝐵)
10	7, 9	sstrd 3954	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝐵)
11		lveclmod 20989	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
12		exsslsb.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
13		eqid 2729	. . . . . . . 8 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
14		exsslsb.k	. . . . . . . 8 ⊢ 𝐾 = (LSpan‘𝑊)
15	12, 13, 14	lspf 20856	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
16	2, 11, 15	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
17	16	ffnd 6671	. . . . 5 ⊢ (𝜑 → 𝐾 Fn 𝒫 𝐵)
18	17	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝐾 Fn 𝒫 𝐵)
19	5	elin2d 4164	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (^◡𝐾 “ {𝐵}))
20		fniniseg 7014	. . . . 5 ⊢ (𝐾 Fn 𝒫 𝐵 → (𝑠 ∈ (^◡𝐾 “ {𝐵}) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ (𝐾‘𝑠) = 𝐵)))
21	20	simplbda 499	. . . 4 ⊢ ((𝐾 Fn 𝒫 𝐵 ∧ 𝑠 ∈ (^◡𝐾 “ {𝐵})) → (𝐾‘𝑠) = 𝐵)
22	18, 19, 21	syl2anc 584	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝐾‘𝑠) = 𝐵)
23	2, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ LMod)
24	23	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑊 ∈ LMod)
25		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊊ 𝑠)
26	25	pssssd 4059	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑠)
27	7	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ⊆ 𝑆)
28	26, 27	sstrd 3954	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑆)
29	9	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ⊆ 𝐵)
30	28, 29	sstrd 3954	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝐵)
31	12, 14	lspssv 20865	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵) → (𝐾‘𝑢) ⊆ 𝐵)
32	24, 30, 31	syl2anc 584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊆ 𝐵)
33		hashf 14279	. . . . . . . . . . . 12 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
34		ffun 6673	. . . . . . . . . . . 12 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
35	33, 34	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ♯)
36		exsslsb.s	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ Fin)
37		pwssfi 9118	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ Fin → (𝑆 ∈ Fin ↔ 𝒫 𝑆 ⊆ Fin))
38	37	ibi 267	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → 𝒫 𝑆 ⊆ Fin)
39	36, 38	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝒫 𝑆 ⊆ Fin)
40	39	ssinss1d 4206	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})) ⊆ Fin)
41	40	sselda 3943	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → 𝑠 ∈ Fin)
42		hashcl 14297	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
43	41, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ ℕ₀)
44		nn0uz 12811	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
45	43, 44	eleqtrdi 2838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ (ℤ_≥‘0))
46	1, 35, 45	funimassd 6909	. . . . . . . . . 10 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
47	46	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
48	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ♯:V⟶(ℕ₀ ∪ {+∞}))
49	48	ffnd 6671	. . . . . . . . . . . 12 ⊢ (𝜑 → ♯ Fn V)
50	49	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ♯ Fn V)
51	50	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ♯ Fn V)
52		vex 3448	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ V)
54	36	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ∈ Fin)
55	54, 28	sselpwd 5278	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝑆)
56	55	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝑆)
57	18	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝐾 Fn 𝒫 𝐵)
58	12	fvexi 6854	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝐵 ∈ V)
60	59, 30	sselpwd 5278	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝐵)
61	60	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝐵)
62		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) = 𝐵)
63		fvex 6853	. . . . . . . . . . . . . 14 ⊢ (𝐾‘𝑢) ∈ V
64	63	elsn 4600	. . . . . . . . . . . . 13 ⊢ ((𝐾‘𝑢) ∈ {𝐵} ↔ (𝐾‘𝑢) = 𝐵)
65	62, 64	sylibr 234	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) ∈ {𝐵})
66	57, 61, 65	elpreimad 7013	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (^◡𝐾 “ {𝐵}))
67	56, 66	elind 4159	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
68	51, 53, 67	fnfvimad 7190	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
69		infssuzle 12866	. . . . . . . . 9 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
70	47, 68, 69	syl2an2r 685	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
71	54, 27	ssfid 9188	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ∈ Fin)
72	71	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑠 ∈ Fin)
73		simplr 768	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊊ 𝑠)
74		hashpss 32707	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠) → (♯‘𝑢) < (♯‘𝑠))
75	72, 73, 74	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < (♯‘𝑠))
76		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
77	75, 76	breqtrd 5128	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
78	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊆ 𝑠)
79	72, 78	ssfid 9188	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ Fin)
80		hashcl 14297	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℕ₀)
82	81	nn0red 12480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℝ)
83	72, 42	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℕ₀)
84	83	nn0red 12480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℝ)
85	76, 84	eqeltrrd 2829	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ ℝ)
86	82, 85	ltnled 11297	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ((♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ↔ ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢)))
87	77, 86	mpbid 232	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
88	70, 87	pm2.65da 816	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ¬ (𝐾‘𝑢) = 𝐵)
89	88	neqned 2932	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ≠ 𝐵)
90		df-pss 3931	. . . . . 6 ⊢ ((𝐾‘𝑢) ⊊ 𝐵 ↔ ((𝐾‘𝑢) ⊆ 𝐵 ∧ (𝐾‘𝑢) ≠ 𝐵))
91	32, 89, 90	sylanbrc 583	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊊ 𝐵)
92	91	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
93	92	alrimiv 1927	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
94		exsslsb.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
95	12, 94, 14	islbs3 21041	. . . 4 ⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))))
96	95	biimpar 477	. . 3 ⊢ ((𝑊 ∈ LVec ∧ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))) → 𝑠 ∈ 𝐽)
97	3, 10, 22, 93, 96	syl13anc 1374	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝐽)
98	36	elexd 3468	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
99		pwidg 4579	. . . . . . . 8 ⊢ (𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆)
100	36, 99	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑆)
101	36, 8	elpwd 4565	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)
102		exsslsb.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)
103		fvex 6853	. . . . . . . . . 10 ⊢ (𝐾‘𝑆) ∈ V
104	103	elsn 4600	. . . . . . . . 9 ⊢ ((𝐾‘𝑆) ∈ {𝐵} ↔ (𝐾‘𝑆) = 𝐵)
105	102, 104	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘𝑆) ∈ {𝐵})
106	17, 101, 105	elpreimad 7013	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (^◡𝐾 “ {𝐵}))
107	100, 106	elind 4159	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
108	49, 98, 107	fnfvimad 7190	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
109	108	ne0d 4301	. . . 4 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅)
110		infssuzcl 12867	. . . 4 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
111	46, 109, 110	syl2anc 584	. . 3 ⊢ (𝜑 → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
112		fvelima2 6895	. . 3 ⊢ ((♯ Fn V ∧ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
113	49, 111, 112	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
114	1, 97, 7, 113	reximd2a 3245	1 ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 ∀wal 1538 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3444 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ⊊ wpss 3912 ∅c0 4292 𝒫 cpw 4559 {csn 4585 class class class wbr 5102 ^◡ccnv 5630 “ cima 5634 Fun wfun 6493 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 Fincfn 8895 infcinf 9368 ℝcr 11043 0cc0 11044 +∞cpnf 11181 < clt 11184 ≤ cle 11185 ℕ₀cn0 12418 ℤ_≥cuz 12769 ♯chash 14271 Basecbs 17155 LModclmod 20742 LSubSpclss 20813 LSpanclspn 20853 LBasisclbs 20957 LVecclvec 20985

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-tpos 8182 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-oadd 8415 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-inf 9370 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-xnn0 12492 df-z 12506 df-uz 12770 df-fz 13445 df-hash 14272 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-0g 17380 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-grp 18844 df-minusg 18845 df-sbg 18846 df-cmn 19688 df-abl 19689 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-drng 20616 df-lmod 20744 df-lss 20814 df-lsp 20854 df-lbs 20958 df-lvec 20986

This theorem is referenced by: lbslelsp 33566

W3C validator