tendoex - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tendoex		Structured version Visualization version GIF version

Theorem tendoex 40313

Description: Generalization of Lemma K of [Crawley] p. 118, cdlemk 40312. TODO: can this be used to shorten uses of cdlemk 40312? (Contributed by NM, 15-Oct-2013.)

**Hypotheses**
Ref	Expression
tendoex.l	⊢ ≤ = (le‘𝐾)
tendoex.h	⊢ 𝐻 = (LHyp‘𝐾)
tendoex.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoex.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
tendoex.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
tendoex	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)

Distinct variable groups: 𝑢,𝐸 𝑢,𝐹 𝑢,𝐾 𝑢,𝑁 𝑢,𝑅 𝑢,𝑇 𝑢,𝑊 Allowed substitution hints: 𝐻(𝑢) ≤ (𝑢)

Proof of Theorem tendoex Dummy variable ℎ is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1l 1223	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL)
2		hlop 38699	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
3	1, 2	syl 17	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ OP)
4		simpl1 1190	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
5		simpl2r 1226	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝑁 ∈ 𝑇)
6		eqid 2731	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		tendoex.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
8		tendoex.t	. . . . . . . 8 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9		tendoex.r	. . . . . . . 8 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
10	6, 7, 8, 9	trlcl 39502	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ (Base‘𝐾))
11	4, 5, 10	syl2anc 583	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝑁) ∈ (Base‘𝐾))
12		simpr 484	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
13		simpl3 1192	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝑁) ≤ (𝑅‘𝐹))
14		tendoex.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
15		eqid 2731	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
16		eqid 2731	. . . . . . 7 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
17	6, 14, 15, 16	leat 38630	. . . . . 6 ⊢ (((𝐾 ∈ OP ∧ (𝑅‘𝑁) ∈ (Base‘𝐾) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾)))
18	3, 11, 12, 13, 17	syl31anc 1372	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾)))
19		simp3 1137	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → (𝑅‘𝑁) ≤ (𝑅‘𝐹))
20		breq2 5152	. . . . . . . . 9 ⊢ ((𝑅‘𝐹) = (0.‘𝐾) → ((𝑅‘𝑁) ≤ (𝑅‘𝐹) ↔ (𝑅‘𝑁) ≤ (0.‘𝐾)))
21	19, 20	syl5ibcom 244	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝐹) = (0.‘𝐾) → (𝑅‘𝑁) ≤ (0.‘𝐾)))
22	21	imp 406	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) ≤ (0.‘𝐾))
23		simpl1l 1223	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐾 ∈ HL)
24	23, 2	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐾 ∈ OP)
25		simpl1 1190	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
26		simpl2r 1226	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝑁 ∈ 𝑇)
27	25, 26, 10	syl2anc 583	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) ∈ (Base‘𝐾))
28	6, 14, 15	ople0 38524	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ (𝑅‘𝑁) ∈ (Base‘𝐾)) → ((𝑅‘𝑁) ≤ (0.‘𝐾) ↔ (𝑅‘𝑁) = (0.‘𝐾)))
29	24, 27, 28	syl2anc 583	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → ((𝑅‘𝑁) ≤ (0.‘𝐾) ↔ (𝑅‘𝑁) = (0.‘𝐾)))
30	22, 29	mpbid 231	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) = (0.‘𝐾))
31	30	olcd 871	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾)))
32		simp1 1135	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
33		simp2l 1198	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → 𝐹 ∈ 𝑇)
34	15, 16, 7, 8, 9	trlator0 39509	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
35	32, 33, 34	syl2anc 583	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
36	18, 31, 35	mpjaodan 956	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾)))
37	36	3expa 1117	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾)))
38		eqcom 2738	. . . . 5 ⊢ ((𝑅‘𝑁) = (𝑅‘𝐹) ↔ (𝑅‘𝐹) = (𝑅‘𝑁))
39		tendoex.e	. . . . . . 7 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
40	7, 8, 9, 39	cdlemk 40312	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
41	40	3expa 1117	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
42	38, 41	sylan2b 593	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
43		eqid 2731	. . . . . . 7 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))
44	6, 7, 8, 39, 43	tendo0cl 40128	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸)
45	44	ad2antrr 723	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸)
46		simplrl 774	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → 𝐹 ∈ 𝑇)
47	43, 6	tendo02 40125	. . . . . . 7 ⊢ (𝐹 ∈ 𝑇 → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾)))
48	46, 47	syl 17	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾)))
49	6, 15, 7, 8, 9	trlid0b 39516	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝑁) = (0.‘𝐾)))
50	49	adantrl 713	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝑁) = (0.‘𝐾)))
51	50	biimpar 477	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → 𝑁 = ( I ↾ (Base‘𝐾)))
52	48, 51	eqtr4d 2774	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁)
53		fveq1 6890	. . . . . . 7 ⊢ (𝑢 = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) → (𝑢‘𝐹) = ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹))
54	53	eqeq1d 2733	. . . . . 6 ⊢ (𝑢 = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) → ((𝑢‘𝐹) = 𝑁 ↔ ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁))
55	54	rspcev 3612	. . . . 5 ⊢ (((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸 ∧ ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
56	45, 52, 55	syl2anc 583	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
57	42, 56	jaodan 955	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
58	37, 57	syldan 590	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)
59	58	3impa 1109	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∃wrex 3069 class class class wbr 5148 ↦ cmpt 5231 I cid 5573 ↾ cres 5678 ‘cfv 6543 Basecbs 17151 lecple 17211 0.cp0 18386 OPcops 38509 Atomscatm 38600 HLchlt 38687 LHypclh 39322 LTrncltrn 39439 trLctrl 39496 TEndoctendo 40090

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-riotaBAD 38290

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7979 df-2nd 7980 df-undef 8264 df-map 8828 df-proset 18258 df-poset 18276 df-plt 18293 df-lub 18309 df-glb 18310 df-join 18311 df-meet 18312 df-p0 18388 df-p1 18389 df-lat 18395 df-clat 18462 df-oposet 38513 df-ol 38515 df-oml 38516 df-covers 38603 df-ats 38604 df-atl 38635 df-cvlat 38659 df-hlat 38688 df-llines 38836 df-lplanes 38837 df-lvols 38838 df-lines 38839 df-psubsp 38841 df-pmap 38842 df-padd 39134 df-lhyp 39326 df-laut 39327 df-ldil 39442 df-ltrn 39443 df-trl 39497 df-tendo 40093

This theorem is referenced by: dva1dim 40323 dihjatcclem4 40759

W3C validator