dihglbcpreN - Mathbox for Norm Megill

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

Theorem dihglbcpreN 41261

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane 𝑊. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dihglbc.b	⊢ 𝐵 = (Base‘𝐾)
dihglbc.g	⊢ 𝐺 = (glb‘𝐾)
dihglbc.h	⊢ 𝐻 = (LHyp‘𝐾)
dihglbc.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dihglbc.l	⊢ ≤ = (le‘𝐾)
dihglbcpre.j	⊢ ∨ = (join‘𝐾)
dihglbcpre.m	⊢ ∧ = (meet‘𝐾)
dihglbcpre.a	⊢ 𝐴 = (Atoms‘𝐾)
dihglbcpre.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
dihglbcpre.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dihglbcpre.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dihglbcpre.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dihglbcpre.f	⊢ 𝐹 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)

**Assertion**
Ref	Expression
dihglbcpreN	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Distinct variable groups: 𝑥,𝑞, ∧ 𝑔,𝑞,𝑥, ≤ 𝑥, ∨ 𝐴,𝑔,𝑞,𝑥 𝐵,𝑞,𝑥 𝑥,𝐸 𝑥,𝐹 𝐺,𝑞,𝑥 𝑔,𝐻,𝑞,𝑥 𝐼,𝑞 𝑔,𝐾,𝑞,𝑥 𝑃,𝑔 𝑥,𝑅 𝑆,𝑞,𝑥 𝑇,𝑔,𝑥 𝑔,𝑊,𝑞,𝑥 Allowed substitution hints: 𝐵(𝑔) 𝑃(𝑥,𝑞) 𝑅(𝑔,𝑞) 𝑆(𝑔) 𝑇(𝑞) 𝐸(𝑔,𝑞) 𝐹(𝑔,𝑞) 𝐺(𝑔) 𝐼(𝑥,𝑔) ∨ (𝑔,𝑞) ∧ (𝑔)

Proof of Theorem dihglbcpreN Dummy variables 𝑓 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dihglbc.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		dihglbc.i	. . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
3	1, 2	dihvalrel 41240	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(𝐺‘𝑆)))
4	3	3ad2ant1 1133	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel (𝐼‘(𝐺‘𝑆)))
5		simp2r 1200	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ≠ ∅)
6		n0 4333	. . . . . 6 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑆)
7	5, 6	sylib 218	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 𝑥 ∈ 𝑆)
8		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
9		simpl1 1191	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2	dihvalrel 41240	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑥))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → Rel (𝐼‘𝑥))
12	8, 11	jca 511	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
13	12	ex 412	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
14	13	eximdv 1916	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
15	7, 14	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
16		df-rex 3060	. . . 4 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
17	15, 16	sylibr 234	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥))
18		reliin 5807	. . 3 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
19	17, 18	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
20		id 22	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊))
21		simp1 1136	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22		simp1l 1197	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
23		hlclat 39318	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
24	22, 23	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
25		simp2l 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
26		dihglbc.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
27		dihglbc.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
28	26, 27	clatglbcl 18519	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
29	24, 25, 28	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
30		simp3 1138	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ¬ (𝐺‘𝑆) ≤ 𝑊)
31		dihglbc.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
32		dihglbcpre.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
33		dihglbcpre.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
34		dihglbcpre.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
35	26, 31, 32, 33, 34, 1	lhpmcvr2 39985	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
36	21, 29, 30, 35	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
37		simpl1 1191	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	29	adantr 480	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐺‘𝑆) ∈ 𝐵)
39		simpl3 1193	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → ¬ (𝐺‘𝑆) ≤ 𝑊)
40		simpr 484	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
41		dihglbcpre.p	. . . . . . . . . 10 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
42		dihglbcpre.t	. . . . . . . . . 10 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
43		dihglbcpre.r	. . . . . . . . . 10 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
44		dihglbcpre.e	. . . . . . . . . 10 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
45		dihglbcpre.f	. . . . . . . . . 10 ⊢ 𝐹 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)
46		vex 3467	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
47		vex 3467	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41210	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
49	37, 38, 39, 40, 48	syl121anc 1376	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
50		simpl2r 1227	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → 𝑆 ≠ ∅)
51		r19.28zv 4481	. . . . . . . . . . 11 ⊢ (𝑆 ≠ ∅ → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
53		simp11 1203	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simp12l 1286	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
55		simp3 1138	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
56	54, 55	sseldd 3964	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
57		simp13 1205	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ (𝐺‘𝑆) ≤ 𝑊)
58		simp11l 1284	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL)
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
60	26, 31, 27	clatglble 18531	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
61	59, 54, 55, 60	syl3anc 1372	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
62	58	hllatd 39324	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat)
63	29	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
64		simp11r 1285	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻)
65	26, 1	lhpbase 39959	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵)
67	26, 31	lattr 18458	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
68	62, 63, 56, 66, 67	syl13anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
69	61, 68	mpand 695	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ≤ 𝑊 → (𝐺‘𝑆) ≤ 𝑊))
70	57, 69	mtod 198	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ≤ 𝑊)
71		simp2l 1199	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
72		simp2ll 1240	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐴)
73	26, 34	atbase 39249	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵)
74	72, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐵)
75	26, 33	latmcl 18454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
76	62, 63, 66, 75	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
77	26, 31, 32	latlej1 18462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
78	62, 74, 76, 77	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
79		simp2r 1200	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))
80	78, 79	breqtrd 5149	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝐺‘𝑆))
81	26, 31, 62, 74, 63, 56, 80, 61	lattrd 18460	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ 𝑥)
82	26, 31, 32, 33, 34	atmod3i1 39825	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ 𝑞 ≤ 𝑥) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
83	58, 72, 56, 66, 81, 82	syl131anc 1384	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
84		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (1.‘𝐾) = (1.‘𝐾)
85	31, 32, 84, 34, 1	lhpjat2 39982	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
86	53, 71, 85	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
87	86	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (𝑞 ∨ 𝑊)) = (𝑥 ∧ (1.‘𝐾)))
88		hlol 39321	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
89	58, 88	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ OL)
90	26, 33, 84	olm11 39187	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
91	89, 56, 90	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
92	83, 87, 91	3eqtrd 2773	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)
93	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41210	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
94	53, 56, 70, 71, 92, 93	syl122anc 1380	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
95	94	3expa 1118	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
96	95	ralbidva 3163	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
97		simp11l 1284	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ HL)
98	97, 23	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ CLat)
99		simp11 1203	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
100		simp3l 1201	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑓 ∈ 𝑇)
101		simp3r 1202	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
102	31, 34, 1, 41	lhpocnel2 39980	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
103	99, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
104		simp2l 1199	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
105	31, 34, 1, 42, 45	ltrniotacl 40540	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
106	99, 103, 104, 105	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐹 ∈ 𝑇)
107	1, 42, 44	tendocl 40728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
108	99, 101, 106, 107	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑠‘𝐹) ∈ 𝑇)
109	1, 42	ltrncnv 40107	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠‘𝐹) ∈ 𝑇) → ^◡(𝑠‘𝐹) ∈ 𝑇)
110	99, 108, 109	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ^◡(𝑠‘𝐹) ∈ 𝑇)
111	1, 42	ltrnco 40680	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇 ∧ ^◡(𝑠‘𝐹) ∈ 𝑇) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
112	99, 100, 110, 111	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
113	26, 1, 42, 43	trlcl 40125	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
114	99, 112, 113	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
115		simp12l 1286	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑆 ⊆ 𝐵)
116	26, 31, 27	clatleglb 18532	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CLat ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
117	98, 114, 115, 116	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
118	117	3expa 1118	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
119	118	pm5.32da 579	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
120	52, 96, 119	3bitr4rd 312	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
121		opex 5449	. . . . . . . . . 10 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
122		eliin 4976	. . . . . . . . . 10 ⊢ (⟨𝑓, 𝑠⟩ ∈ V → (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥))
124	120, 123	bitr4di 289	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
125	49, 124	bitrd 279	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
126	125	exp44 437	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → ((𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))))
127	126	imp4a 422	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))))
128	127	rexlimdv 3140	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))
129	36, 128	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
130	129	eqrelrdv2 5785	. 2 ⊢ (((Rel (𝐼‘(𝐺‘𝑆)) ∧ Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
131	4, 19, 20, 130	syl21anc 837	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ∃wrex 3059 Vcvv 3463 ⊆ wss 3931 ∅c0 4313 ⟨cop 4612 ∩ ciin 4972 class class class wbr 5123 ^◡ccnv 5664 ∘ ccom 5669 Rel wrel 5670 ‘cfv 6541 ℩crio 7369 (class class class)co 7413 Basecbs 17229 lecple 17280 occoc 17281 glbcglb 18326 joincjn 18327 meetcmee 18328 1.cp1 18438 Latclat 18445 CLatccla 18512 OLcol 39134 Atomscatm 39223 HLchlt 39310 LHypclh 39945 LTrncltrn 40062 trLctrl 40119 TEndoctendo 40713 DIsoHcdih 41189

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-riotaBAD 38913

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-tpos 8233 df-undef 8280 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-er 8727 df-map 8850 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-n0 12510 df-z 12597 df-uz 12861 df-fz 13530 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-sca 17289 df-vsca 17290 df-0g 17457 df-proset 18310 df-poset 18329 df-plt 18344 df-lub 18360 df-glb 18361 df-join 18362 df-meet 18363 df-p0 18439 df-p1 18440 df-lat 18446 df-clat 18513 df-mgm 18622 df-sgrp 18701 df-mnd 18717 df-submnd 18766 df-grp 18923 df-minusg 18924 df-sbg 18925 df-subg 19110 df-cntz 19304 df-lsm 19622 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-oppr 20302 df-dvdsr 20325 df-unit 20326 df-invr 20356 df-dvr 20369 df-drng 20699 df-lmod 20828 df-lss 20898 df-lsp 20938 df-lvec 21070 df-oposet 39136 df-ol 39138 df-oml 39139 df-covers 39226 df-ats 39227 df-atl 39258 df-cvlat 39282 df-hlat 39311 df-llines 39459 df-lplanes 39460 df-lvols 39461 df-lines 39462 df-psubsp 39464 df-pmap 39465 df-padd 39757 df-lhyp 39949 df-laut 39950 df-ldil 40065 df-ltrn 40066 df-trl 40120 df-tendo 40716 df-edring 40718 df-disoa 40990 df-dvech 41040 df-dib 41100 df-dic 41134 df-dih 41190

This theorem is referenced by: dihglbcN 41262

W3C validator