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 39241

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 39220	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(𝐺‘𝑆)))
4	3	3ad2ant1 1131	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel (𝐼‘(𝐺‘𝑆)))
5		simp2r 1198	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ≠ ∅)
6		n0 4277	. . . . . 6 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑆)
7	5, 6	sylib 217	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 𝑥 ∈ 𝑆)
8		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
9		simpl1 1189	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2	dihvalrel 39220	. . . . . . . . 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 1921	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
15	7, 14	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
16		df-rex 3069	. . . 4 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
17	15, 16	sylibr 233	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥))
18		reliin 5716	. . 3 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
19	17, 18	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
20		id 22	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊))
21		simp1 1134	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22		simp1l 1195	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
23		hlclat 37299	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
24	22, 23	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
25		simp2l 1197	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
26		dihglbc.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
27		dihglbc.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
28	26, 27	clatglbcl 18138	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
29	24, 25, 28	syl2anc 583	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
30		simp3 1136	. . . . 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 37965	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
36	21, 29, 30, 35	syl12anc 833	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
37		simpl1 1189	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	29	adantr 480	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐺‘𝑆) ∈ 𝐵)
39		simpl3 1191	. . . . . . . . 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 3426	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
47		vex 3426	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 39190	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
49	37, 38, 39, 40, 48	syl121anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
50		simpl2r 1225	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → 𝑆 ≠ ∅)
51		r19.28zv 4428	. . . . . . . . . . 11 ⊢ (𝑆 ≠ ∅ → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
53		simp11 1201	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simp12l 1284	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
55		simp3 1136	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
56	54, 55	sseldd 3918	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
57		simp13 1203	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ (𝐺‘𝑆) ≤ 𝑊)
58		simp11l 1282	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL)
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
60	26, 31, 27	clatglble 18150	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
61	59, 54, 55, 60	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
62	58	hllatd 37305	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat)
63	29	3ad2ant1 1131	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
64		simp11r 1283	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻)
65	26, 1	lhpbase 37939	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵)
67	26, 31	lattr 18077	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
68	62, 63, 56, 66, 67	syl13anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
69	61, 68	mpand 691	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ≤ 𝑊 → (𝐺‘𝑆) ≤ 𝑊))
70	57, 69	mtod 197	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ≤ 𝑊)
71		simp2l 1197	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
72		simp2ll 1238	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐴)
73	26, 34	atbase 37230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵)
74	72, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐵)
75	26, 33	latmcl 18073	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
76	62, 63, 66, 75	syl3anc 1369	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
77	26, 31, 32	latlej1 18081	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
78	62, 74, 76, 77	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
79		simp2r 1198	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))
80	78, 79	breqtrd 5096	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝐺‘𝑆))
81	26, 31, 62, 74, 63, 56, 80, 61	lattrd 18079	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ 𝑥)
82	26, 31, 32, 33, 34	atmod3i1 37805	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ 𝑞 ≤ 𝑥) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
83	58, 72, 56, 66, 81, 82	syl131anc 1381	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
84		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (1.‘𝐾) = (1.‘𝐾)
85	31, 32, 84, 34, 1	lhpjat2 37962	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
86	53, 71, 85	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
87	86	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (𝑞 ∨ 𝑊)) = (𝑥 ∧ (1.‘𝐾)))
88		hlol 37302	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
89	58, 88	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ OL)
90	26, 33, 84	olm11 37168	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
91	89, 56, 90	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
92	83, 87, 91	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)
93	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 39190	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
94	53, 56, 70, 71, 92, 93	syl122anc 1377	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
95	94	3expa 1116	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
96	95	ralbidva 3119	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
97		simp11l 1282	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ HL)
98	97, 23	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ CLat)
99		simp11 1201	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
100		simp3l 1199	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑓 ∈ 𝑇)
101		simp3r 1200	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
102	31, 34, 1, 41	lhpocnel2 37960	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
103	99, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
104		simp2l 1197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
105	31, 34, 1, 42, 45	ltrniotacl 38520	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
106	99, 103, 104, 105	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐹 ∈ 𝑇)
107	1, 42, 44	tendocl 38708	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
108	99, 101, 106, 107	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑠‘𝐹) ∈ 𝑇)
109	1, 42	ltrncnv 38087	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠‘𝐹) ∈ 𝑇) → ^◡(𝑠‘𝐹) ∈ 𝑇)
110	99, 108, 109	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ^◡(𝑠‘𝐹) ∈ 𝑇)
111	1, 42	ltrnco 38660	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇 ∧ ^◡(𝑠‘𝐹) ∈ 𝑇) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
112	99, 100, 110, 111	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
113	26, 1, 42, 43	trlcl 38105	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
114	99, 112, 113	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
115		simp12l 1284	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑆 ⊆ 𝐵)
116	26, 31, 27	clatleglb 18151	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CLat ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
117	98, 114, 115, 116	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
118	117	3expa 1116	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
119	118	pm5.32da 578	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
120	52, 96, 119	3bitr4rd 311	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
121		opex 5373	. . . . . . . . . 10 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
122		eliin 4926	. . . . . . . . . 10 ⊢ (⟨𝑓, 𝑠⟩ ∈ V → (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥))
124	120, 123	bitr4di 288	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
125	49, 124	bitrd 278	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
126	125	exp44 437	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → ((𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))))
127	126	imp4a 422	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))))
128	127	rexlimdv 3211	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))
129	36, 128	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
130	129	eqrelrdv2 5694	. 2 ⊢ (((Rel (𝐼‘(𝐺‘𝑆)) ∧ Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
131	4, 19, 20, 130	syl21anc 834	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∃wex 1783 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ⊆ wss 3883 ∅c0 4253 ⟨cop 4564 ∩ ciin 4922 class class class wbr 5070 ^◡ccnv 5579 ∘ ccom 5584 Rel wrel 5585 ‘cfv 6418 ℩crio 7211 (class class class)co 7255 Basecbs 16840 lecple 16895 occoc 16896 glbcglb 17943 joincjn 17944 meetcmee 17945 1.cp1 18057 Latclat 18064 CLatccla 18131 OLcol 37115 Atomscatm 37204 HLchlt 37291 LHypclh 37925 LTrncltrn 38042 trLctrl 38099 TEndoctendo 38693 DIsoHcdih 39169

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-riotaBAD 36894

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-tpos 8013 df-undef 8060 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-sca 16904 df-vsca 16905 df-0g 17069 df-proset 17928 df-poset 17946 df-plt 17963 df-lub 17979 df-glb 17980 df-join 17981 df-meet 17982 df-p0 18058 df-p1 18059 df-lat 18065 df-clat 18132 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-submnd 18346 df-grp 18495 df-minusg 18496 df-sbg 18497 df-subg 18667 df-cntz 18838 df-lsm 19156 df-cmn 19303 df-abl 19304 df-mgp 19636 df-ur 19653 df-ring 19700 df-oppr 19777 df-dvdsr 19798 df-unit 19799 df-invr 19829 df-dvr 19840 df-drng 19908 df-lmod 20040 df-lss 20109 df-lsp 20149 df-lvec 20280 df-oposet 37117 df-ol 37119 df-oml 37120 df-covers 37207 df-ats 37208 df-atl 37239 df-cvlat 37263 df-hlat 37292 df-llines 37439 df-lplanes 37440 df-lvols 37441 df-lines 37442 df-psubsp 37444 df-pmap 37445 df-padd 37737 df-lhyp 37929 df-laut 37930 df-ldil 38045 df-ltrn 38046 df-trl 38100 df-tendo 38696 df-edring 38698 df-disoa 38970 df-dvech 39020 df-dib 39080 df-dic 39114 df-dih 39170

This theorem is referenced by: dihglbcN 39242

W3C validator