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 41763

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 41742	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(𝐺‘𝑆)))
4	3	3ad2ant1 1134	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel (𝐼‘(𝐺‘𝑆)))
5		simp2r 1202	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ≠ ∅)
6		n0 4294	. . . . . 6 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑆)
7	5, 6	sylib 218	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 𝑥 ∈ 𝑆)
8		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
9		simpl1 1193	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2	dihvalrel 41742	. . . . . . . . 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 1919	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
15	7, 14	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
16		df-rex 3063	. . . 4 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
17	15, 16	sylibr 234	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥))
18		reliin 5767	. . 3 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
19	17, 18	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
20		id 22	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊))
21		simp1 1137	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22		simp1l 1199	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
23		hlclat 39821	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
24	22, 23	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
25		simp2l 1201	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
26		dihglbc.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
27		dihglbc.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
28	26, 27	clatglbcl 18465	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
29	24, 25, 28	syl2anc 585	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
30		simp3 1139	. . . . 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 40487	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
36	21, 29, 30, 35	syl12anc 837	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
37		simpl1 1193	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	29	adantr 480	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐺‘𝑆) ∈ 𝐵)
39		simpl3 1195	. . . . . . . . 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 3434	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
47		vex 3434	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41712	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
49	37, 38, 39, 40, 48	syl121anc 1378	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
50		simpl2r 1229	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → 𝑆 ≠ ∅)
51		r19.28zv 4447	. . . . . . . . . . 11 ⊢ (𝑆 ≠ ∅ → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
53		simp11 1205	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simp12l 1288	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
55		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
56	54, 55	sseldd 3923	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
57		simp13 1207	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ (𝐺‘𝑆) ≤ 𝑊)
58		simp11l 1286	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL)
59	58, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
60	26, 31, 27	clatglble 18477	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
61	59, 54, 55, 60	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
62	58	hllatd 39827	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat)
63	29	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
64		simp11r 1287	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻)
65	26, 1	lhpbase 40461	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵)
67	26, 31	lattr 18404	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
68	62, 63, 56, 66, 67	syl13anc 1375	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
69	61, 68	mpand 696	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ≤ 𝑊 → (𝐺‘𝑆) ≤ 𝑊))
70	57, 69	mtod 198	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ≤ 𝑊)
71		simp2l 1201	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
72		simp2ll 1242	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐴)
73	26, 34	atbase 39752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵)
74	72, 73	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐵)
75	26, 33	latmcl 18400	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
76	62, 63, 66, 75	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
77	26, 31, 32	latlej1 18408	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
78	62, 74, 76, 77	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
79		simp2r 1202	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))
80	78, 79	breqtrd 5112	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝐺‘𝑆))
81	26, 31, 62, 74, 63, 56, 80, 61	lattrd 18406	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ 𝑥)
82	26, 31, 32, 33, 34	atmod3i1 40327	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ 𝑞 ≤ 𝑥) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
83	58, 72, 56, 66, 81, 82	syl131anc 1386	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
84		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (1.‘𝐾) = (1.‘𝐾)
85	31, 32, 84, 34, 1	lhpjat2 40484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
86	53, 71, 85	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
87	86	oveq2d 7377	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (𝑞 ∨ 𝑊)) = (𝑥 ∧ (1.‘𝐾)))
88		hlol 39824	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
89	58, 88	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ OL)
90	26, 33, 84	olm11 39690	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
91	89, 56, 90	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
92	83, 87, 91	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)
93	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 41712	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
94	53, 56, 70, 71, 92, 93	syl122anc 1382	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
95	94	3expa 1119	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
96	95	ralbidva 3159	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
97		simp11l 1286	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ HL)
98	97, 23	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ CLat)
99		simp11 1205	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
100		simp3l 1203	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑓 ∈ 𝑇)
101		simp3r 1204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
102	31, 34, 1, 41	lhpocnel2 40482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
103	99, 102	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
104		simp2l 1201	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
105	31, 34, 1, 42, 45	ltrniotacl 41042	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
106	99, 103, 104, 105	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐹 ∈ 𝑇)
107	1, 42, 44	tendocl 41230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
108	99, 101, 106, 107	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑠‘𝐹) ∈ 𝑇)
109	1, 42	ltrncnv 40609	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠‘𝐹) ∈ 𝑇) → ^◡(𝑠‘𝐹) ∈ 𝑇)
110	99, 108, 109	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ^◡(𝑠‘𝐹) ∈ 𝑇)
111	1, 42	ltrnco 41182	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇 ∧ ^◡(𝑠‘𝐹) ∈ 𝑇) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
112	99, 100, 110, 111	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
113	26, 1, 42, 43	trlcl 40627	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
114	99, 112, 113	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
115		simp12l 1288	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑆 ⊆ 𝐵)
116	26, 31, 27	clatleglb 18478	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CLat ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
117	98, 114, 115, 116	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
118	117	3expa 1119	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
119	118	pm5.32da 579	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
120	52, 96, 119	3bitr4rd 312	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
121		opex 5412	. . . . . . . . . 10 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
122		eliin 4939	. . . . . . . . . 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 3137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))
129	36, 128	mpd 15	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
130	129	eqrelrdv2 5745	. 2 ⊢ (((Rel (𝐼‘(𝐺‘𝑆)) ∧ Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
131	4, 19, 20, 130	syl21anc 838	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ⊆ wss 3890 ∅c0 4274 ⟨cop 4574 ∩ ciin 4935 class class class wbr 5086 ^◡ccnv 5624 ∘ ccom 5629 Rel wrel 5630 ‘cfv 6493 ℩crio 7317 (class class class)co 7361 Basecbs 17173 lecple 17221 occoc 17222 glbcglb 18270 joincjn 18271 meetcmee 18272 1.cp1 18382 Latclat 18391 CLatccla 18458 OLcol 39637 Atomscatm 39726 HLchlt 39813 LHypclh 40447 LTrncltrn 40564 trLctrl 40621 TEndoctendo 41215 DIsoHcdih 41691

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-riotaBAD 39416

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-tpos 8170 df-undef 8217 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-n0 12432 df-z 12519 df-uz 12783 df-fz 13456 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-sca 17230 df-vsca 17231 df-0g 17398 df-proset 18254 df-poset 18273 df-plt 18288 df-lub 18304 df-glb 18305 df-join 18306 df-meet 18307 df-p0 18383 df-p1 18384 df-lat 18392 df-clat 18459 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-subg 19093 df-cntz 19286 df-lsm 19605 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-dvr 20375 df-drng 20702 df-lmod 20851 df-lss 20921 df-lsp 20961 df-lvec 21093 df-oposet 39639 df-ol 39641 df-oml 39642 df-covers 39729 df-ats 39730 df-atl 39761 df-cvlat 39785 df-hlat 39814 df-llines 39961 df-lplanes 39962 df-lvols 39963 df-lines 39964 df-psubsp 39966 df-pmap 39967 df-padd 40259 df-lhyp 40451 df-laut 40452 df-ldil 40567 df-ltrn 40568 df-trl 40622 df-tendo 41218 df-edring 41220 df-disoa 41492 df-dvech 41542 df-dib 41602 df-dic 41636 df-dih 41692

This theorem is referenced by: dihglbcN 41764

W3C validator