exsslsb

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

	Ref	Expression
Hypotheses	exsslsb.b	$⊢ B = {Base}_{W}$
	exsslsb.j	$⊢ J = LBasis (W)$
	exsslsb.k	$⊢ K = LSpan (W)$
	exsslsb.w	$⊢ φ \to W \in LVec$
	exsslsb.s	$⊢ φ \to S \in Fin$
	exsslsb.1	$⊢ φ \to S \subseteq B$
	exsslsb.2	$⊢ φ \to K (S) = B$
Assertion	exsslsb	$⊢ φ \to \exists s \in J s \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		exsslsb.b	$⊢ B = {Base}_{W}$
2		exsslsb.j	$⊢ J = LBasis (W)$
3		exsslsb.k	$⊢ K = LSpan (W)$
4		exsslsb.w	$⊢ φ \to W \in LVec$
5		exsslsb.s	$⊢ φ \to S \in Fin$
6		exsslsb.1	$⊢ φ \to S \subseteq B$
7		exsslsb.2	$⊢ φ \to K (S) = B$
8		nfv	$⊢ Ⅎ s φ$
9	4	ad2antrr	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to W \in LVec$
10		simplr	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))$
11	10	elin2d	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \in (𝒫 S \cap K^{-1} [\{B\}])$
12	11	elin1d	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \in 𝒫 S$
13	12	elpwid	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \subseteq S$
14	6	ad2antrr	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to S \subseteq B$
15	13 14	sstrd	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \subseteq B$
16		lveclmod	$⊢ W \in LVec \to W \in LMod$
17		eqid	$⊢ LSubSp (W) = LSubSp (W)$
18	1 17 3	lspf	$⊢ W \in LMod \to K : 𝒫 B ⟶ LSubSp (W)$
19	4 16 18	3syl	$⊢ φ \to K : 𝒫 B ⟶ LSubSp (W)$
20	19	ffnd	$⊢ φ \to K Fn 𝒫 B$
21	20	ad2antrr	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to K Fn 𝒫 B$
22	11	elin2d	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \in K^{-1} [\{B\}]$
23		fniniseg	$⊢ K Fn 𝒫 B \to (s \in K^{-1} [\{B\}] \leftrightarrow (s \in 𝒫 B \land K (s) = B))$
24	23	simplbda	$⊢ (K Fn 𝒫 B \land s \in K^{-1} [\{B\}]) \to K (s) = B$
25	21 22 24	syl2anc	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to K (s) = B$
26	4 16	syl	$⊢ φ \to W \in LMod$
27	26	ad3antrrr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to W \in LMod$
28		simpr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \subset s$
29	28	pssssd	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \subseteq s$
30	13	adantr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to s \subseteq S$
31	29 30	sstrd	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \subseteq S$
32	14	adantr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to S \subseteq B$
33	31 32	sstrd	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \subseteq B$
34	1 3	lspssv	$⊢ (W \in LMod \land u \subseteq B) \to K (u) \subseteq B$
35	27 33 34	syl2anc	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to K (u) \subseteq B$
36		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
37		ffun	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to Fun \|.\|$
38	36 37	mp1i	$⊢ φ \to Fun \|.\|$
39		pwssfi	$⊢ S \in Fin \to (S \in Fin \leftrightarrow 𝒫 S \subseteq Fin)$
40	39	ibi	$⊢ S \in Fin \to 𝒫 S \subseteq Fin$
41	5 40	syl	$⊢ φ \to 𝒫 S \subseteq Fin$
42	41	ssinss1d	$⊢ φ \to 𝒫 S \cap K^{-1} [\{B\}] \subseteq Fin$
43	42	sselda	$⊢ (φ \land s \in (𝒫 S \cap K^{-1} [\{B\}])) \to s \in Fin$
44		hashcl	$⊢ s \in Fin \to \|s\| \in ℕ_{0}$
45	43 44	syl	$⊢ (φ \land s \in (𝒫 S \cap K^{-1} [\{B\}])) \to \|s\| \in ℕ_{0}$
46		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
47	45 46	eleqtrdi	$⊢ (φ \land s \in (𝒫 S \cap K^{-1} [\{B\}])) \to \|s\| \in ℤ_{\geq 0}$
48	8 38 47	funimassd	$⊢ φ \to \|.\| [𝒫 S \cap K^{-1} [\{B\}]] \subseteq ℤ_{\geq 0}$
49	48	ad3antrrr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to \|.\| [𝒫 S \cap K^{-1} [\{B\}]] \subseteq ℤ_{\geq 0}$
50	36	a1i	$⊢ φ \to \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
51	50	ffnd	$⊢ φ \to \|.\| Fn V$
52	51	ad3antrrr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to \|.\| Fn V$
53	52	adantr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|.\| Fn V$
54		vex	$⊢ u \in V$
55	54	a1i	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in V$
56	5	ad3antrrr	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to S \in Fin$
57	56 31	sselpwd	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \in 𝒫 S$
58	57	adantr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in 𝒫 S$
59	21	ad2antrr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to K Fn 𝒫 B$
60	1	fvexi	$⊢ B \in V$
61	60	a1i	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to B \in V$
62	61 33	sselpwd	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to u \in 𝒫 B$
63	62	adantr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in 𝒫 B$
64		simpr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to K (u) = B$
65		fvex	$⊢ K (u) \in V$
66	65	elsn	$⊢ K (u) \in \{B\} \leftrightarrow K (u) = B$
67	64 66	sylibr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to K (u) \in \{B\}$
68	59 63 67	elpreimad	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in K^{-1} [\{B\}]$
69	58 68	elind	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in (𝒫 S \cap K^{-1} [\{B\}])$
70	53 55 69	fnfvimad	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|u\| \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]$
71		infssuzle	$⊢ (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] \subseteq ℤ_{\geq 0} \land \|u\| \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]) \to inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \leq \|u\|$
72	49 70 71	syl2an2r	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \leq \|u\|$
73	56 30	ssfid	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to s \in Fin$
74	73	adantr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to s \in Fin$
75		simplr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \subset s$
76		hashpss	$⊢ (s \in Fin \land u \subset s) \to \|u\| < \|s\|$
77	74 75 76	syl2anc	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|u\| < \|s\|$
78		simpllr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)$
79	77 78	breqtrd	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|u\| < inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)$
80	29	adantr	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \subseteq s$
81	74 80	ssfid	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to u \in Fin$
82		hashcl	$⊢ u \in Fin \to \|u\| \in ℕ_{0}$
83	81 82	syl	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|u\| \in ℕ_{0}$
84	83	nn0red	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|u\| \in ℝ$
85	74 44	syl	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|s\| \in ℕ_{0}$
86	85	nn0red	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \|s\| \in ℝ$
87	78 86	eqeltrrd	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \in ℝ$
88	84 87	ltnled	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to (\|u\| < inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \leftrightarrow \neg inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \leq \|u\|)$
89	79 88	mpbid	$⊢ ((((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \land K (u) = B) \to \neg inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \leq \|u\|$
90	72 89	pm2.65da	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to \neg K (u) = B$
91	90	neqned	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to K (u) \neq B$
92		df-pss	$⊢ K (u) \subset B \leftrightarrow (K (u) \subseteq B \land K (u) \neq B)$
93	35 91 92	sylanbrc	$⊢ (((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \land u \subset s) \to K (u) \subset B$
94	93	ex	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to (u \subset s \to K (u) \subset B)$
95	94	alrimiv	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to \forall u (u \subset s \to K (u) \subset B)$
96	1 2 3	islbs3	$⊢ W \in LVec \to (s \in J \leftrightarrow (s \subseteq B \land K (s) = B \land \forall u (u \subset s \to K (u) \subset B)))$
97	96	biimpar	$⊢ (W \in LVec \land (s \subseteq B \land K (s) = B \land \forall u (u \subset s \to K (u) \subset B))) \to s \in J$
98	9 15 25 95 97	syl13anc	$⊢ ((φ \land s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}]))) \land \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)) \to s \in J$
99	5	elexd	$⊢ φ \to S \in V$
100		pwidg	$⊢ S \in Fin \to S \in 𝒫 S$
101	5 100	syl	$⊢ φ \to S \in 𝒫 S$
102	5 6	elpwd	$⊢ φ \to S \in 𝒫 B$
103		fvex	$⊢ K (S) \in V$
104	103	elsn	$⊢ K (S) \in \{B\} \leftrightarrow K (S) = B$
105	7 104	sylibr	$⊢ φ \to K (S) \in \{B\}$
106	20 102 105	elpreimad	$⊢ φ \to S \in K^{-1} [\{B\}]$
107	101 106	elind	$⊢ φ \to S \in (𝒫 S \cap K^{-1} [\{B\}])$
108	51 99 107	fnfvimad	$⊢ φ \to \|S\| \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]$
109	108	ne0d	$⊢ φ \to \|.\| [𝒫 S \cap K^{-1} [\{B\}]] \neq \emptyset$
110		infssuzcl	$⊢ (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] \subseteq ℤ_{\geq 0} \land \|.\| [𝒫 S \cap K^{-1} [\{B\}]] \neq \emptyset) \to inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]$
111	48 109 110	syl2anc	$⊢ φ \to inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]$
112		fvelima2	$⊢ (\|.\| Fn V \land inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <) \in \|.\| [𝒫 S \cap K^{-1} [\{B\}]]) \to \exists s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}])) \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)$
113	51 111 112	syl2anc	$⊢ φ \to \exists s \in (V \cap (𝒫 S \cap K^{-1} [\{B\}])) \|s\| = inf (\|.\| [𝒫 S \cap K^{-1} [\{B\}]] ℝ <)$
114	8 98 13 113	reximd2a	$⊢ φ \to \exists s \in J s \subseteq S$

Metamath Proof Explorer

Theorem exsslsb

Proof