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 34027

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 4158	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
6	5	elin1d 4157	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝒫 𝑆)
7	6	elpwid 4573	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝑆)
8		exsslsb.1	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
9	8	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑆 ⊆ 𝐵)
10	7, 9	sstrd 3948	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ⊆ 𝐵)
11		lveclmod 21257	. . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
12		exsslsb.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
13		eqid 2765	. . . . . . . 8 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
14		exsslsb.k	. . . . . . . 8 ⊢ 𝐾 = (LSpan‘𝑊)
15	12, 13, 14	lspf 21125	. . . . . . 7 ⊢ (𝑊 ∈ LMod → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
16	2, 11, 15	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝐾:𝒫 𝐵⟶(LSubSp‘𝑊))
17	16	ffnd 6710	. . . . 5 ⊢ (𝜑 → 𝐾 Fn 𝒫 𝐵)
18	17	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝐾 Fn 𝒫 𝐵)
19	5	elin2d 4158	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ (^◡𝐾 “ {𝐵}))
20		fniniseg 7059	. . . . 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 4055	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑠)
27	7	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ⊆ 𝑆)
28	26, 27	sstrd 3948	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝑆)
29	9	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ⊆ 𝐵)
30	28, 29	sstrd 3948	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ⊆ 𝐵)
31	12, 14	lspssv 21134	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑢 ⊆ 𝐵) → (𝐾‘𝑢) ⊆ 𝐵)
32	24, 30, 31	syl2anc 596	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ⊆ 𝐵)
33		hashf 14388	. . . . . . . . . . . 12 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
34		ffun 6712	. . . . . . . . . . . 12 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
35	33, 34	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ♯)
36		exsslsb.s	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ∈ Fin)
37		pwssfi 9164	. . . . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → 𝑠 ∈ Fin)
42		hashcl 14406	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
43	41, 42	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ ℕ₀)
44		nn0uz 12912	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
45	43, 44	eleqtrdi 2875	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) → (♯‘𝑠) ∈ (ℤ_≥‘0))
46	1, 35, 45	funimassd 6951	. . . . . . . . . 10 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
47	46	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0))
48	33	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ♯:V⟶(ℕ₀ ∪ {+∞}))
49	48	ffnd 6710	. . . . . . . . . . . 12 ⊢ (𝜑 → ♯ Fn V)
50	49	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → ♯ Fn V)
51	50	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → ♯ Fn V)
52		vex 3461	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
53	52	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ V)
54	36	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑆 ∈ Fin)
55	54, 28	sselpwd 5301	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝑆)
56	55	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝑆)
57	18	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝐾 Fn 𝒫 𝐵)
58	12	fvexi 6899	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝐵 ∈ V)
60	59, 30	sselpwd 5301	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑢 ∈ 𝒫 𝐵)
61	60	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ 𝒫 𝐵)
62		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) = 𝐵)
63		fvex 6898	. . . . . . . . . . . . . 14 ⊢ (𝐾‘𝑢) ∈ V
64	63	elsn 4606	. . . . . . . . . . . . 13 ⊢ ((𝐾‘𝑢) ∈ {𝐵} ↔ (𝐾‘𝑢) = 𝐵)
65	62, 64	sylibr 237	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (𝐾‘𝑢) ∈ {𝐵})
66	57, 61, 65	elpreimad 7058	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (^◡𝐾 “ {𝐵}))
67	56, 66	elind 4153	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
68	51, 53, 67	fnfvimad 7236	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
69		infssuzle 12967	. . . . . . . . 9 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯‘𝑢) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
70	47, 68, 69	syl2an2r 698	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ≤ (♯‘𝑢))
71	54, 27	ssfid 9232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → 𝑠 ∈ Fin)
72	71	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑠 ∈ Fin)
73		simplr 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊊ 𝑠)
74		hashpss 14460	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ Fin ∧ 𝑢 ⊊ 𝑠) → (♯‘𝑢) < (♯‘𝑠))
75	72, 73, 74	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < (♯‘𝑠))
76		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
77	75, 76	breqtrd 5139	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) < inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
78	26	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ⊆ 𝑠)
79	72, 78	ssfid 9232	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → 𝑢 ∈ Fin)
80		hashcl 14406	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ₀)
81	79, 80	syl 18	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℕ₀)
82	81	nn0red 12577	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑢) ∈ ℝ)
83	72, 42	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℕ₀)
84	83	nn0red 12577	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → (♯‘𝑠) ∈ ℝ)
85	76, 84	eqeltrrd 2866	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) ∧ (𝐾‘𝑢) = 𝐵) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ ℝ)
86	82, 85	ltnled 11368	. . . . . . . . 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 2967	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) ∧ 𝑢 ⊊ 𝑠) → (𝐾‘𝑢) ≠ 𝐵)
90		df-pss 3926	. . . . . 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 21309	. . . 4 ⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))))
96	95	biimpar 483	. . 3 ⊢ ((𝑊 ∈ LVec ∧ (𝑠 ⊆ 𝐵 ∧ (𝐾‘𝑠) = 𝐵 ∧ ∀𝑢(𝑢 ⊊ 𝑠 → (𝐾‘𝑢) ⊊ 𝐵))) → 𝑠 ∈ 𝐽)
97	3, 10, 22, 93, 96	syl13anc 1399	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) ∧ (♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < )) → 𝑠 ∈ 𝐽)
98	36	elexd 3480	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ V)
99		pwidg 4584	. . . . . . . 8 ⊢ (𝑆 ∈ Fin → 𝑆 ∈ 𝒫 𝑆)
100	36, 99	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑆)
101	36, 8	elpwd 4570	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵)
102		exsslsb.2	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)
103		fvex 6898	. . . . . . . . . 10 ⊢ (𝐾‘𝑆) ∈ V
104	103	elsn 4606	. . . . . . . . 9 ⊢ ((𝐾‘𝑆) ∈ {𝐵} ↔ (𝐾‘𝑆) = 𝐵)
105	102, 104	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘𝑆) ∈ {𝐵})
106	17, 101, 105	elpreimad 7058	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (^◡𝐾 “ {𝐵}))
107	100, 106	elind 4153	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))
108	49, 98, 107	fnfvimad 7236	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
109	108	ne0d 4295	. . . 4 ⊢ (𝜑 → (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅)
110		infssuzcl 12968	. . . 4 ⊢ (((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ⊆ (ℤ_≥‘0) ∧ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))) ≠ ∅) → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
111	46, 109, 110	syl2anc 596	. . 3 ⊢ (𝜑 → inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))))
112		fvelima2 6937	. . 3 ⊢ ((♯ Fn V ∧ inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ) ∈ (♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))) → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
113	49, 111, 112	syl2anc 596	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (V ∩ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵})))(♯‘𝑠) = inf((♯ “ (𝒫 𝑆 ∩ (^◡𝐾 “ {𝐵}))), ℝ, < ))
114	1, 97, 7, 113	reximd2a 3277	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 2146 ≠ wne 2960 ∃wrex 3091 Vcvv 3457 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ⊊ wpss 3907 ∅c0 4286 𝒫 cpw 4564 {csn 4591 class class class wbr 5111 ^◡ccnv 5662 “ cima 5666 Fun wfun 6534 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 Fincfn 8945 infcinf 9404 ℝcr 11110 0cc0 11111 +∞cpnf 11251 < clt 11254 ≤ cle 11255 ℕ₀cn0 12515 ℤ_≥cuz 12874 ♯chash 14380 Basecbs 17287 LModclmod 21011 LSubSpclss 21082 LSpanclspn 21122 LBasisclbs 21225 LVecclvec 21253

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 df-tpos 8224 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-oadd 8459 df-er 8696 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-sup 9405 df-inf 9406 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-nn 12245 df-2 12314 df-3 12315 df-n0 12516 df-xnn0 12589 df-z 12603 df-uz 12875 df-fz 13548 df-hash 14381 df-sets 17242 df-slot 17260 df-ndx 17272 df-base 17288 df-ress 17309 df-plusg 17341 df-mulr 17342 df-0g 17512 df-mgm 18716 df-sgrp 18799 df-mnd 18815 df-grp 19027 df-minusg 19028 df-sbg 19029 df-cmn 19876 df-abl 19877 df-mgp 20241 df-rng 20255 df-ur 20288 df-ring 20341 df-oppr 20445 df-dvdsr 20465 df-unit 20466 df-invr 20496 df-drng 20859 df-lmod 21013 df-lss 21083 df-lsp 21123 df-lbs 21226 df-lvec 21254

This theorem is used by: lbslelsp 34028

W3C validator