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 41929

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 41908	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(𝐺‘𝑆)))
4	3	3ad2ant1 1147	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel (𝐼‘(𝐺‘𝑆)))
5		simp2r 1215	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ≠ ∅)
6		n0 4307	. . . . . 6 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑆)
7	5, 6	sylib 220	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 𝑥 ∈ 𝑆)
8		simpr 488	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
9		simpl1 1206	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2	dihvalrel 41908	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑥))
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → Rel (𝐼‘𝑥))
12	8, 11	jca 519	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
13	12	ex 416	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
14	13	eximdv 1939	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
15	7, 14	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
16		df-rex 3089	. . . 4 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
17	15, 16	sylibr 236	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥))
18		reliin 5792	. . 3 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
19	17, 18	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
20		id 22	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊))
21		simp1 1150	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22		simp1l 1212	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
23		hlclat 39987	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
24	22, 23	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
25		simp2l 1214	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
26		dihglbc.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
27		dihglbc.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
28	26, 27	clatglbcl 18539	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
29	24, 25, 28	syl2anc 593	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
30		simp3 1152	. . . . 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 40653	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
36	21, 29, 30, 35	syl12anc 847	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
37		simpl1 1206	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	29	adantr 484	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐺‘𝑆) ∈ 𝐵)
39		simpl3 1208	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → ¬ (𝐺‘𝑆) ≤ 𝑊)
40		simpr 488	. . . . . . . . 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 3460	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
47		vex 3460	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41878	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
49	37, 38, 39, 40, 48	syl121anc 1396	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
50		simpl2r 1242	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → 𝑆 ≠ ∅)
51		r19.28zv 4462	. . . . . . . . . . 11 ⊢ (𝑆 ≠ ∅ → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
53		simp11 1218	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simp12l 1301	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
55		simp3 1152	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
56	54, 55	sseldd 3939	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
57		simp13 1220	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ (𝐺‘𝑆) ≤ 𝑊)
58		simp11l 1299	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL)
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
60	26, 31, 27	clatglble 18551	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
61	59, 54, 55, 60	syl3anc 1392	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
62	58	hllatd 39993	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat)
63	29	3ad2ant1 1147	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
64		simp11r 1300	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻)
65	26, 1	lhpbase 40627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵)
67	26, 31	lattr 18478	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
68	62, 63, 56, 66, 67	syl13anc 1393	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
69	61, 68	mpand 705	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ≤ 𝑊 → (𝐺‘𝑆) ≤ 𝑊))
70	57, 69	mtod 200	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ≤ 𝑊)
71		simp2l 1214	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
72		simp2ll 1255	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐴)
73	26, 34	atbase 39918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵)
74	72, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐵)
75	26, 33	latmcl 18474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
76	62, 63, 66, 75	syl3anc 1392	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
77	26, 31, 32	latlej1 18482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
78	62, 74, 76, 77	syl3anc 1392	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
79		simp2r 1215	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))
80	78, 79	breqtrd 5128	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝐺‘𝑆))
81	26, 31, 62, 74, 63, 56, 80, 61	lattrd 18480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ 𝑥)
82	26, 31, 32, 33, 34	atmod3i1 40493	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ 𝑞 ≤ 𝑥) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
83	58, 72, 56, 66, 81, 82	syl131anc 1404	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
84		eqid 2764	. . . . . . . . . . . . . . . . 17 ⊢ (1.‘𝐾) = (1.‘𝐾)
85	31, 32, 84, 34, 1	lhpjat2 40650	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
86	53, 71, 85	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
87	86	oveq2d 7414	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (𝑞 ∨ 𝑊)) = (𝑥 ∧ (1.‘𝐾)))
88		hlol 39990	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
89	58, 88	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ OL)
90	26, 33, 84	olm11 39856	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
91	89, 56, 90	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
92	83, 87, 91	3eqtrd 2803	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)
93	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41878	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
94	53, 56, 70, 71, 92, 93	syl122anc 1400	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
95	94	3expa 1132	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
96	95	ralbidva 3185	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
97		simp11l 1299	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ HL)
98	97, 23	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ CLat)
99		simp11 1218	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
100		simp3l 1216	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑓 ∈ 𝑇)
101		simp3r 1217	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
102	31, 34, 1, 41	lhpocnel2 40648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
103	99, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
104		simp2l 1214	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
105	31, 34, 1, 42, 45	ltrniotacl 41208	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
106	99, 103, 104, 105	syl3anc 1392	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐹 ∈ 𝑇)
107	1, 42, 44	tendocl 41396	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
108	99, 101, 106, 107	syl3anc 1392	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑠‘𝐹) ∈ 𝑇)
109	1, 42	ltrncnv 40775	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠‘𝐹) ∈ 𝑇) → ^◡(𝑠‘𝐹) ∈ 𝑇)
110	99, 108, 109	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ^◡(𝑠‘𝐹) ∈ 𝑇)
111	1, 42	ltrnco 41348	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇 ∧ ^◡(𝑠‘𝐹) ∈ 𝑇) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
112	99, 100, 110, 111	syl3anc 1392	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
113	26, 1, 42, 43	trlcl 40793	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
114	99, 112, 113	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
115		simp12l 1301	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑆 ⊆ 𝐵)
116	26, 31, 27	clatleglb 18552	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CLat ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
117	98, 114, 115, 116	syl3anc 1392	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
118	117	3expa 1132	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
119	118	pm5.32da 587	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
120	52, 96, 119	3bitr4rd 314	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
121		opex 5433	. . . . . . . . . 10 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
122		eliin 4956	. . . . . . . . . 10 ⊢ (⟨𝑓, 𝑠⟩ ∈ V → (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥))
124	120, 123	bitr4di 291	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
125	49, 124	bitrd 281	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
126	125	exp44 441	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → ((𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))))
127	126	imp4a 426	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))))
128	127	rexlimdv 3163	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))
129	36, 128	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
130	129	eqrelrdv2 5769	. 2 ⊢ (((Rel (𝐼‘(𝐺‘𝑆)) ∧ Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
131	4, 19, 20, 130	syl21anc 848	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1099 = wceq 1562 ∃wex 1801 ∈ wcel 2144 ≠ wne 2959 ∀wral 3078 ∃wrex 3088 Vcvv 3456 ⊆ wss 3906 ∅c0 4287 ⟨cop 4590 ∩ ciin 4952 class class class wbr 5102 ^◡ccnv 5648 ∘ ccom 5653 Rel wrel 5654 ‘cfv 6523 ℩crio 7354 (class class class)co 7398 Basecbs 17247 lecple 17295 occoc 17296 glbcglb 18344 joincjn 18345 meetcmee 18346 1.cp1 18456 Latclat 18465 CLatccla 18532 OLcol 39803 Atomscatm 39892 HLchlt 39979 LHypclh 40613 LTrncltrn 40730 trLctrl 40787 TEndoctendo 41381 DIsoHcdih 41857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-riotaBAD 39582

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-tpos 8208 df-undef 8255 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-er 8680 df-map 8812 df-en 8930 df-dom 8931 df-sdom 8932 df-fin 8933 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-nn 12213 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-n0 12484 df-z 12571 df-uz 12842 df-fz 13515 df-struct 17185 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17248 df-ress 17269 df-plusg 17301 df-mulr 17302 df-sca 17304 df-vsca 17305 df-0g 17472 df-proset 18328 df-poset 18347 df-plt 18362 df-lub 18378 df-glb 18379 df-join 18380 df-meet 18381 df-p0 18457 df-p1 18458 df-lat 18466 df-clat 18533 df-mgm 18676 df-sgrp 18755 df-mnd 18771 df-submnd 18820 df-grp 18980 df-minusg 18981 df-sbg 18982 df-subg 19167 df-cntz 19359 df-lsm 19678 df-cmn 19824 df-abl 19825 df-mgp 20189 df-rng 20201 df-ur 20234 df-ring 20287 df-oppr 20388 df-dvdsr 20408 df-unit 20409 df-invr 20439 df-dvr 20452 df-drng 20783 df-lmod 20931 df-lss 21001 df-lsp 21041 df-lvec 21172 df-oposet 39805 df-ol 39807 df-oml 39808 df-covers 39895 df-ats 39896 df-atl 39927 df-cvlat 39951 df-hlat 39980 df-llines 40127 df-lplanes 40128 df-lvols 40129 df-lines 40130 df-psubsp 40132 df-pmap 40133 df-padd 40425 df-lhyp 40617 df-laut 40618 df-ldil 40733 df-ltrn 40734 df-trl 40788 df-tendo 41384 df-edring 41386 df-disoa 41658 df-dvech 41708 df-dib 41768 df-dic 41802 df-dih 41858

This theorem is referenced by: dihglbcN 41930

W3C validator