Theorem islbs 19841

Description: The predicate "𝐵 is a basis for the left module or vector space 𝑊". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 14-Jan-2015.)

Hypotheses

Ref	Expression
islbs.v	⊢ 𝑉 = (Base‘𝑊)
islbs.f	⊢ 𝐹 = (Scalar‘𝑊)
islbs.s	⊢ · = ( ·𝑠 ‘𝑊)
islbs.k	⊢ 𝐾 = (Base‘𝐹)
islbs.j	⊢ 𝐽 = (LBasis‘𝑊)
islbs.n	⊢ 𝑁 = (LSpan‘𝑊)
islbs.z	⊢ 0 = (0g‘𝐹)

Assertion

Ref	Expression
islbs	⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑦,𝐾   𝑥,𝑁,𝑦   𝑥,𝑊,𝑦   𝑥,𝐹,𝑦   𝑦, 0

Allowed substitution hints:   · (𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥)   𝑉(𝑥,𝑦)   𝑋(𝑥,𝑦)   0 (𝑥)

Proof of Theorem islbs

Dummy variables 𝑏 𝑓 𝑛 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3459	. . . 4 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
2		islbs.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
3		fveq2 6645	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4		islbs.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑊)
5	3, 4	eqtr4di 2851	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
6	5	pweqd 4516	. . . . . . 7 ⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7		fvexd 6660	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) ∈ V)
8		fveq2 6645	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
9		islbs.n	. . . . . . . . 9 ⊢ 𝑁 = (LSpan‘𝑊)
10	8, 9	eqtr4di 2851	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁)
11		fvexd 6660	. . . . . . . . 9 ⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) ∈ V)
12		fveq2 6645	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
13	12	adantr 484	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = (Scalar‘𝑊))
14		islbs.f	. . . . . . . . . 10 ⊢ 𝐹 = (Scalar‘𝑊)
15	13, 14	eqtr4di 2851	. . . . . . . . 9 ⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = 𝐹)
16		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑛 = 𝑁)
17	16	fveq1d 6647	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘𝑏) = (𝑁‘𝑏))
18	5	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑤) = 𝑉)
19	17, 18	eqeq12d 2814	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑛‘𝑏) = (Base‘𝑤) ↔ (𝑁‘𝑏) = 𝑉))
20		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
21	20	fveq2d 6649	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
22		islbs.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝐹)
23	21, 22	eqtr4di 2851	. . . . . . . . . . . . 13 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
24	20	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = (0g‘𝐹))
25		islbs.z	. . . . . . . . . . . . . . 15 ⊢ 0 = (0g‘𝐹)
26	24, 25	eqtr4di 2851	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = 0 )
27	26	sneqd 4537	. . . . . . . . . . . . 13 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → {(0g‘𝑓)} = { 0 })
28	23, 27	difeq12d 4051	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((Base‘𝑓) ∖ {(0g‘𝑓)}) = (𝐾 ∖ { 0 }))
29		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
30		islbs.s	. . . . . . . . . . . . . . . . 17 ⊢ · = ( ·𝑠 ‘𝑊)
31	29, 30	eqtr4di 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
32	31	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ( ·𝑠 ‘𝑤) = · )
33	32	oveqd 7152	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑦( ·𝑠 ‘𝑤)𝑥) = (𝑦 · 𝑥))
34	16	fveq1d 6647	. . . . . . . . . . . . . 14 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝑏 ∖ {𝑥})))
35	33, 34	eleq12d 2884	. . . . . . . . . . . . 13 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
36	35	notbid 321	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
37	28, 36	raleqbidv 3354	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
38	37	ralbidv 3162	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
39	19, 38	anbi12d 633	. . . . . . . . 9 ⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
40	11, 15, 39	sbcied2 3763	. . . . . . . 8 ⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → ([(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
41	7, 10, 40	sbcied2 3763	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ([(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
42	6, 41	rabeqbidv 3433	. . . . . 6 ⊢ (𝑤 = 𝑊 → {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
43		df-lbs 19840	. . . . . 6 ⊢ LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
44	4	fvexi 6659	. . . . . . . 8 ⊢ 𝑉 ∈ V
45	44	pwex 5246	. . . . . . 7 ⊢ 𝒫 𝑉 ∈ V
46	45	rabex 5199	. . . . . 6 ⊢ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ∈ V
47	42, 43, 46	fvmpt 6745	. . . . 5 ⊢ (𝑊 ∈ V → (LBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
48	2, 47	syl5eq 2845	. . . 4 ⊢ (𝑊 ∈ V → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
49	1, 48	syl 17	. . 3 ⊢ (𝑊 ∈ 𝑋 → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
50	49	eleq2d 2875	. 2 ⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ 𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}))
51	44	elpw2 5212	. . . 4 ⊢ (𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉)
52	51	anbi1i 626	. . 3 ⊢ ((𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
53		fveqeq2 6654	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑁‘𝑏) = 𝑉 ↔ (𝑁‘𝐵) = 𝑉))
54		difeq1 4043	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑏 ∖ {𝑥}) = (𝐵 ∖ {𝑥}))
55	54	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝑁‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑥})))
56	55	eleq2d 2875	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
57	56	notbid 321	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
58	57	ralbidv 3162	. . . . . 6 ⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
59	58	raleqbi1dv 3356	. . . . 5 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
60	53, 59	anbi12d 633	. . . 4 ⊢ (𝑏 = 𝐵 → (((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
61	60	elrab 3628	. . 3 ⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
62		3anass 1092	. . 3 ⊢ ((𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
63	52, 61, 62	3bitr4i 306	. 2 ⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
64	50, 63	syl6bb 290	1 ⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3441  [wsbc 3720   ∖ cdif 3878   ⊆ wss 3881  𝒫 cpw 4497  {csn 4525  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  Scalarcsca 16560   ·_𝑠 cvsca 16561  0_gc0g 16705  LSpanclspn 19736  LBasisclbs 19839

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332  df-ov 7138  df-lbs 19840

This theorem is referenced by:  lbsss  19842  lbssp  19844  lbsind  19845  lbspropd  19864  islbs2  19919  frlmlbs  20486  islbs4  20521