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 42548

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 42527	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘(𝐺‘𝑆)))
4	3	3ad2ant1 1151	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel (𝐼‘(𝐺‘𝑆)))
5		simp2r 1219	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ≠ ∅)
6		n0 4303	. . . . . 6 ⊢ (𝑆 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑆)
7	5, 6	sylib 221	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 𝑥 ∈ 𝑆)
8		simpr 490	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
9		simpl1 1210	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2	dihvalrel 42527	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑥))
11	9, 10	syl 18	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → Rel (𝐼‘𝑥))
12	8, 11	jca 521	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
13	12	ex 418	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
14	13	eximdv 1952	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥))))
15	7, 14	mpd 16	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
16		df-rex 3091	. . . 4 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ Rel (𝐼‘𝑥)))
17	15, 16	sylibr 237	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥))
18		reliin 5800	. . 3 ⊢ (∃𝑥 ∈ 𝑆 Rel (𝐼‘𝑥) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
19	17, 18	syl 18	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
20		id 23	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊))
21		simp1 1154	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22		simp1l 1216	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL)
23		hlclat 40606	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
24	22, 23	syl 18	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat)
25		simp2l 1218	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵)
26		dihglbc.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
27		dihglbc.g	. . . . . . 7 ⊢ 𝐺 = (glb‘𝐾)
28	26, 27	clatglbcl 18705	. . . . . 6 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
29	24, 25, 28	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) ∈ 𝐵)
30		simp3 1156	. . . . 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 41272	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
36	21, 29, 30, 35	syl12anc 850	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)))
37		simpl1 1210	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	29	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (𝐺‘𝑆) ∈ 𝐵)
39		simpl3 1212	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → ¬ (𝐺‘𝑆) ≤ 𝑊)
40		simpr 490	. . . . . . . . 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 3458	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
47		vex 3458	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
48	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 42497	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
49	37, 38, 39, 40, 48	syl121anc 1403	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆))))
50		simpl2r 1246	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → 𝑆 ≠ ∅)
51		r19.28zv 4465	. . . . . . . . . . 11 ⊢ (𝑆 ≠ ∅ → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
52	50, 51	syl 18	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
53		simp11 1222	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simp12l 1305	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵)
55		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
56	54, 55	sseldd 3914	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
57		simp13 1224	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ (𝐺‘𝑆) ≤ 𝑊)
58		simp11l 1303	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL)
59	58, 23	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat)
60	26, 31, 27	clatglble 18717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
61	59, 54, 55, 60	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑥)
62	58	hllatd 40612	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat)
63	29	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵)
64		simp11r 1304	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻)
65	26, 1	lhpbase 41246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
66	64, 65	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵)
67	26, 31	lattr 18644	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Lat ∧ ((𝐺‘𝑆) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
68	62, 63, 56, 66, 67	syl13anc 1400	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (((𝐺‘𝑆) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊) → (𝐺‘𝑆) ≤ 𝑊))
69	61, 68	mpand 708	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ≤ 𝑊 → (𝐺‘𝑆) ≤ 𝑊))
70	57, 69	mtod 201	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ¬ 𝑥 ≤ 𝑊)
71		simp2l 1218	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
72		simp2ll 1259	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐴)
73	26, 34	atbase 40537	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵)
74	72, 73	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ∈ 𝐵)
75	26, 33	latmcl 18640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
76	62, 63, 66, 75	syl3anc 1399	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵)
77	26, 31, 32	latlej1 18648	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ((𝐺‘𝑆) ∧ 𝑊) ∈ 𝐵) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
78	62, 74, 76, 77	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)))
79		simp2r 1219	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))
80	78, 79	breqtrd 5134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ (𝐺‘𝑆))
81	26, 31, 62, 74, 63, 56, 80, 61	lattrd 18646	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝑞 ≤ 𝑥)
82	26, 31, 32, 33, 34	atmod3i1 41112	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ 𝑞 ≤ 𝑥) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
83	58, 72, 56, 66, 81, 82	syl131anc 1411	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = (𝑥 ∧ (𝑞 ∨ 𝑊)))
84		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (1.‘𝐾) = (1.‘𝐾)
85	31, 32, 84, 34, 1	lhpjat2 41269	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
86	53, 71, 85	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ 𝑊) = (1.‘𝐾))
87	86	oveq2d 7456	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (𝑞 ∨ 𝑊)) = (𝑥 ∧ (1.‘𝐾)))
88		hlol 40609	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
89	58, 88	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ OL)
90	26, 33, 84	olm11 40475	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
91	89, 56, 90	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ (1.‘𝐾)) = 𝑥)
92	83, 87, 91	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)
93	26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47	dihopelvalc 42497	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ (𝑥 ∧ 𝑊)) = 𝑥)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
94	53, 56, 70, 71, 92, 93	syl122anc 1407	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
95	94	3expa 1136	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ 𝑥 ∈ 𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
96	95	ralbidva 3187	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
97		simp11l 1303	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ HL)
98	97, 23	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐾 ∈ CLat)
99		simp11 1222	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
100		simp3l 1220	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑓 ∈ 𝑇)
101		simp3r 1221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
102	31, 34, 1, 41	lhpocnel2 41267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
103	99, 102	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
104		simp2l 1218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊))
105	31, 34, 1, 42, 45	ltrniotacl 41827	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
106	99, 103, 104, 105	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐹 ∈ 𝑇)
107	1, 42, 44	tendocl 42015	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
108	99, 101, 106, 107	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑠‘𝐹) ∈ 𝑇)
109	1, 42	ltrncnv 41394	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠‘𝐹) ∈ 𝑇) → ^◡(𝑠‘𝐹) ∈ 𝑇)
110	99, 108, 109	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ^◡(𝑠‘𝐹) ∈ 𝑇)
111	1, 42	ltrnco 41967	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇 ∧ ^◡(𝑠‘𝐹) ∈ 𝑇) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
112	99, 100, 110, 111	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇)
113	26, 1, 42, 43	trlcl 41412	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∘ ^◡(𝑠‘𝐹)) ∈ 𝑇) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
114	99, 112, 113	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵)
115		simp12l 1305	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝑆 ⊆ 𝐵)
116	26, 31, 27	clatleglb 18718	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ CLat ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
117	98, 114, 115, 116	syl3anc 1399	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
118	117	3expa 1136	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ((𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥))
119	118	pm5.32da 590	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ ∀𝑥 ∈ 𝑆 (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ 𝑥)))
120	52, 96, 119	3bitr4rd 315	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
121		opex 5436	. . . . . . . . . 10 ⊢ ⟨𝑓, 𝑠⟩ ∈ V
122		eliin 4959	. . . . . . . . . 10 ⊢ (⟨𝑓, 𝑠⟩ ∈ V → (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥)))
123	121, 122	ax-mp 5	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥) ↔ ∀𝑥 ∈ 𝑆 ⟨𝑓, 𝑠⟩ ∈ (𝐼‘𝑥))
124	120, 123	bitr4di 292	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑅‘(𝑓 ∘ ^◡(𝑠‘𝐹))) ≤ (𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
125	49, 124	bitrd 282	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆))) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
126	125	exp44 443	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → (¬ 𝑞 ≤ 𝑊 → ((𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))))
127	126	imp4a 428	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝑞 ∈ 𝐴 → ((¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))))
128	127	rexlimdv 3165	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ (𝑞 ∨ ((𝐺‘𝑆) ∧ 𝑊)) = (𝐺‘𝑆)) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))))
129	36, 128	mpd 16	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (⟨𝑓, 𝑠⟩ ∈ (𝐼‘(𝐺‘𝑆)) ↔ ⟨𝑓, 𝑠⟩ ∈ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)))
130	129	eqrelrdv2 5776	. 2 ⊢ (((Rel (𝐼‘(𝐺‘𝑆)) ∧ Rel ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) ∧ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))
131	4, 19, 20, 130	syl21anc 851	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∅c0 4281 ⟨cop 4838 ∩ ciin 4955 class class class wbr 5106 ^◡ccnv 5654 ∘ ccom 5659 Rel wrel 5660 ‘cfv 6555 ℩crio 7396 (class class class)co 7440 Basecbs 17413 lecple 17461 occoc 17462 glbcglb 18510 joincjn 18511 meetcmee 18512 1.cp1 18622 Latclat 18631 CLatccla 18698 OLcol 40422 Atomscatm 40511 HLchlt 40598 LHypclh 41232 LTrncltrn 41349 trLctrl 41406 TEndoctendo 42000 DIsoHcdih 42476

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-riotaBAD 40201

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-tpos 8268 df-undef 8315 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-er 8742 df-map 8874 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-n0 12631 df-z 12718 df-uz 12990 df-fz 13664 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-sca 17470 df-vsca 17471 df-0g 17638 df-proset 18494 df-poset 18513 df-plt 18528 df-lub 18544 df-glb 18545 df-join 18546 df-meet 18547 df-p0 18623 df-p1 18624 df-lat 18632 df-clat 18699 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-submnd 19005 df-grp 19173 df-minusg 19174 df-sbg 19175 df-subg 19359 df-cntz 19558 df-lsm 19877 df-cmn 20023 df-abl 20024 df-mgp 20388 df-rng 20402 df-ur 20435 df-ring 20488 df-oppr 20594 df-dvdsr 20614 df-unit 20615 df-invr 20645 df-dvr 20658 df-drng 21009 df-lmod 21164 df-lss 21234 df-lsp 21274 df-lvec 21405 df-oposet 40424 df-ol 40426 df-oml 40427 df-covers 40514 df-ats 40515 df-atl 40546 df-cvlat 40570 df-hlat 40599 df-llines 40746 df-lplanes 40747 df-lvols 40748 df-lines 40749 df-psubsp 40751 df-pmap 40752 df-padd 41044 df-lhyp 41236 df-laut 41237 df-ldil 41352 df-ltrn 41353 df-trl 41407 df-tendo 42003 df-edring 42005 df-disoa 42277 df-dvech 42327 df-dib 42387 df-dic 42421 df-dih 42477

This theorem is used by: dihglbcN 42549

W3C validator