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 33774

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 1916	. 2 ⊢ Ⅎ𝑠𝜑
2		exsslsb.w	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LVec)
3	2	ad2antrr 727	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑊 ∈ LVec)
4		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
5	4	elin2d 4159	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
6	5	elin1d 4158	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝒫 𝑆)
7	6	elpwid 4565	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝑆)
8		exsslsb.1	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
9	8	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑆 ⊆ 𝐵)
10	7, 9	sstrd 3946	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝐵)
11		lveclmod 21070	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
12		exsslsb.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
13		eqid 2737	. . . . . . . 8 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
14		exsslsb.k	. . . . . . . 8 ⊢ 𝐾 = (LSpan‘𝑊)
15	12, 13, 14	lspf 20937	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
16	2, 11, 15	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
17	16	ffnd 6671	. . . . 5 ⊢ (𝜑 → 𝐾 Fn 𝒫 𝐵)
18	17	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝐾 Fn 𝒫 𝐵)
19	5	elin2d 4159	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (^◡𝐾 “ {𝐵}))
20		fniniseg 7014	. . . . 5 ⊢ (𝐾 Fn 𝒫 𝐵 → (𝑠 ∈ (^◡𝐾 “ {𝐵}) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ (𝐾‘𝑠) = 𝐵)))
21	20	simplbda 499	. . . 4 ⊢ ((𝐾 Fn 𝒫 𝐵 ∧ 𝑠 ∈ (^◡𝐾 “ {𝐵})) → (𝐾‘𝑠) = 𝐵)
22	18, 19, 21	syl2anc 585	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝐾‘𝑠) = 𝐵)
23	2, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ LMod)
24	23	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑊 ∈ LMod)
25		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊊ 𝑠)
26	25	pssssd 4054	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑠)
27	7	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ⊆ 𝑆)
28	26, 27	sstrd 3946	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑆)
29	9	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ⊆ 𝐵)
30	28, 29	sstrd 3946	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝐵)
31	12, 14	lspssv 20946	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵) → (𝐾‘𝑢) ⊆ 𝐵)
32	24, 30, 31	syl2anc 585	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊆ 𝐵)
33		hashf 14273	. . . . . . . . . . . 12 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
34		ffun 6673	. . . . . . . . . . . 12 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
35	33, 34	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ♯)
36		exsslsb.s	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ Fin)
37		pwssfi 9113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ∈ Fin → (𝑆 ∈ Fin ↔ 𝒫 𝑆 ⊆ Fin))
38	37	ibi 267	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → 𝒫 𝑆 ⊆ Fin)
39	36, 38	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝒫 𝑆 ⊆ Fin)
40	39	ssinss1d 4201	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})) ⊆ Fin)
41	40	sselda 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → 𝑠 ∈ Fin)
42		hashcl 14291	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
43	41, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ ℕ₀)
44		nn0uz 12801	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
45	43, 44	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ (ℤ_≥‘0))
46	1, 35, 45	funimassd 6908	. . . . . . . . . 10 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
47	46	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
48	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ♯:V⟶(ℕ₀ ∪ {+∞}))
49	48	ffnd 6671	. . . . . . . . . . . 12 ⊢ (𝜑 → ♯ Fn V)
50	49	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ♯ Fn V)
51	50	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ♯ Fn V)
52		vex 3446	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ V)
54	36	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ∈ Fin)
55	54, 28	sselpwd 5275	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝑆)
56	55	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝑆)
57	18	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝐾 Fn 𝒫 𝐵)
58	12	fvexi 6856	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝐵 ∈ V)
60	59, 30	sselpwd 5275	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝐵)
61	60	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝐵)
62		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) = 𝐵)
63		fvex 6855	. . . . . . . . . . . . . 14 ⊢ (𝐾‘𝑢) ∈ V
64	63	elsn 4597	. . . . . . . . . . . . 13 ⊢ ((𝐾‘𝑢) ∈ {𝐵} ↔ (𝐾‘𝑢) = 𝐵)
65	62, 64	sylibr 234	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) ∈ {𝐵})
66	57, 61, 65	elpreimad 7013	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (^◡𝐾 “ {𝐵}))
67	56, 66	elind 4154	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
68	51, 53, 67	fnfvimad 7190	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
69		infssuzle 12856	. . . . . . . . 9 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
70	47, 68, 69	syl2an2r 686	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
71	54, 27	ssfid 9181	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ∈ Fin)
72	71	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑠 ∈ Fin)
73		simplr 769	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊊ 𝑠)
74		hashpss 32900	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠) → (♯‘𝑢) < (♯‘𝑠))
75	72, 73, 74	syl2anc 585	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < (♯‘𝑠))
76		simpllr 776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
77	75, 76	breqtrd 5126	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
78	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊆ 𝑠)
79	72, 78	ssfid 9181	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ Fin)
80		hashcl 14291	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℕ₀)
82	81	nn0red 12475	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℝ)
83	72, 42	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℕ₀)
84	83	nn0red 12475	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℝ)
85	76, 84	eqeltrrd 2838	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ ℝ)
86	82, 85	ltnled 11292	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ((♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ↔ ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢)))
87	77, 86	mpbid 232	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ¬ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
88	70, 87	pm2.65da 817	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ¬ (𝐾‘𝑢) = 𝐵)
89	88	neqned 2940	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ≠ 𝐵)
90		df-pss 3923	. . . . . 6 ⊢ ((𝐾‘𝑢) ⊊ 𝐵 ↔ ((𝐾‘𝑢) ⊆ 𝐵 ∧ (𝐾‘𝑢) ≠ 𝐵))
91	32, 89, 90	sylanbrc 584	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊊ 𝐵)
92	91	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → (𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
93	92	alrimiv 1929	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))
94		exsslsb.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
95	12, 94, 14	islbs3 21122	. . . 4 ⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))))
96	95	biimpar 477	. . 3 ⊢ ((𝑊 ∈ LVec ∧ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))) → 𝑠 ∈ 𝐽)
97	3, 10, 22, 93, 96	syl13anc 1375	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝐽)
98	36	elexd 3466	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
99		pwidg 4576	. . . . . . . 8 ⊢ (𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆)
100	36, 99	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑆)
101	36, 8	elpwd 4562	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)
102		exsslsb.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)
103		fvex 6855	. . . . . . . . . 10 ⊢ (𝐾‘𝑆) ∈ V
104	103	elsn 4597	. . . . . . . . 9 ⊢ ((𝐾‘𝑆) ∈ {𝐵} ↔ (𝐾‘𝑆) = 𝐵)
105	102, 104	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘𝑆) ∈ {𝐵})
106	17, 101, 105	elpreimad 7013	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (^◡𝐾 “ {𝐵}))
107	100, 106	elind 4154	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
108	49, 98, 107	fnfvimad 7190	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
109	108	ne0d 4296	. . . 4 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅)
110		infssuzcl 12857	. . . 4 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
111	46, 109, 110	syl2anc 585	. . 3 ⊢ (𝜑 → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
112		fvelima2 6894	. . 3 ⊢ ((♯ Fn V ∧ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
113	49, 111, 112	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
114	1, 97, 7, 113	reximd2a 3248	1 ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 ∀wal 1540 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 Vcvv 3442 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ⊊ wpss 3904 ∅c0 4287 𝒫 cpw 4556 {csn 4582 class class class wbr 5100 ^◡ccnv 5631 “ cima 5635 Fun wfun 6494 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 Fincfn 8895 infcinf 9356 ℝcr 11037 0cc0 11038 +∞cpnf 11175 < clt 11178 ≤ cle 11179 ℕ₀cn0 12413 ℤ_≥cuz 12763 ♯chash 14265 Basecbs 17148 LModclmod 20823 LSubSpclss 20894 LSpanclspn 20934 LBasisclbs 21038 LVecclvec 21066

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-tpos 8178 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-oadd 8411 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-fz 13436 df-hash 14266 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-0g 17373 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-grp 18878 df-minusg 18879 df-sbg 18880 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-ring 20182 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-drng 20676 df-lmod 20825 df-lss 20895 df-lsp 20935 df-lbs 21039 df-lvec 21067

This theorem is referenced by: lbslelsp 33775

W3C validator