Metamath Proof Explorer

Theorem dihglbcpreN

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

Ref Expression
Hypotheses 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 dihglbcpreN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dihglbc.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihglbc.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 dihglbc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihglbc.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dihglbc.l ⊢ ≤ = ( le ‘ 𝐾 )
6 dihglbcpre.j ⊢ ∨ = ( join ‘ 𝐾 )
7 dihglbcpre.m ⊢ ∧ = ( meet ‘ 𝐾 )
8 dihglbcpre.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
9 dihglbcpre.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
10 dihglbcpre.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11 dihglbcpre.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
12 dihglbcpre.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
13 dihglbcpre.f ⊢ 𝐹 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 )
14 3 4 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
15 14 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
16 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑆 ≠ ∅ )
17 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
18 16 17 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∃ 𝑥 𝑥 ∈ 𝑆 )
19 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
20 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 3 4 dihvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑥 ) )
22 20 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑆 ) → Rel ( 𝐼 ‘ 𝑥 ) )
23 19 22 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) )
24 23 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) ) )
25 24 eximdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) ) )
26 18 25 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) )
27 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) )
28 26 27 sylibr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) )
29 reliin ⊢ ( ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) → Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
30 28 29 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
31 id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) )
32 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ HL )
34 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
35 33 34 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝐾 ∈ CLat )
36 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → 𝑆 ⊆ 𝐵 )
37 1 2 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
38 35 36 37 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
39 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 )
40 1 5 6 7 8 3 lhpmcvr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) )
41 32 38 39 40 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) )
42 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
43 38 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
44 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 )
45 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) )
46 vex ⊢ 𝑓 ∈ V
47 vex ⊢ 𝑠 ∈ V
48 1 5 6 7 8 3 9 10 11 12 4 13 46 47 dihopelvalc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
49 42 43 44 45 48 syl121anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
50 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → 𝑆 ≠ ∅ )
51 r19.28zv ⊢ ( 𝑆 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
52 50 51 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
53 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
54 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
55 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
56 54 55 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
57 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 )
58 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ HL )
59 58 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ CLat )
60 1 5 2 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
61 59 54 55 60 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 )
62 58 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ Lat )
63 38 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
64 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ 𝐻 )
65 1 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
66 64 65 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ 𝐵 )
67 1 5 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) )
68 62 63 56 66 67 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝐺 ‘ 𝑆 ) ≤ 𝑥 ∧ 𝑥 ≤ 𝑊 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) )
69 61 68 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ≤ 𝑊 → ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) )
70 57 69 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝑥 ≤ 𝑊 )
71 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
72 simp2ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑞 ∈ 𝐴 )
73 1 8 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵 )
74 72 73 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑞 ∈ 𝐵 )
75 1 7 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
76 62 63 66 75 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 )
77 1 5 6 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑞 ∈ 𝐵 ∧ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ∈ 𝐵 ) → 𝑞 ≤ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) )
78 62 74 76 77 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑞 ≤ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) )
79 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) )
80 78 79 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑞 ≤ ( 𝐺 ‘ 𝑆 ) )
81 1 5 62 74 63 56 80 61 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑞 ≤ 𝑥 )
82 1 5 6 7 8 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑞 ≤ 𝑥 ) → ( 𝑞 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑥 ∧ ( 𝑞 ∨ 𝑊 ) ) )
83 58 72 56 66 81 82 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑞 ∨ ( 𝑥 ∧ 𝑊 ) ) = ( 𝑥 ∧ ( 𝑞 ∨ 𝑊 ) ) )
84 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
85 5 6 84 8 3 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( 𝑞 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
86 53 71 85 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑞 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
87 86 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∧ ( 𝑞 ∨ 𝑊 ) ) = ( 𝑥 ∧ ( 1. ‘ 𝐾 ) ) )
88 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
89 58 88 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ OL )
90 1 7 84 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∧ ( 1. ‘ 𝐾 ) ) = 𝑥 )
91 89 56 90 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∧ ( 1. ‘ 𝐾 ) ) = 𝑥 )
92 83 87 91 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑞 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 )
93 1 5 6 7 8 3 9 10 11 12 4 13 46 47 dihopelvalc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
94 53 56 70 71 92 93 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
95 94 3expa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
96 95 ralbidva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
97 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝐾 ∈ HL )
98 97 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝐾 ∈ CLat )
99 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
100 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝑓 ∈ 𝑇 )
101 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝑠 ∈ 𝐸 )
102 5 8 3 9 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
103 99 102 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
104 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
105 5 8 3 10 13 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
106 99 103 104 105 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝐹 ∈ 𝑇 )
107 3 10 12 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
108 99 101 106 107 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
109 3 10 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ) → ◡ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
110 99 108 109 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ◡ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
111 3 10 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ ◡ ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ∈ 𝑇 )
112 99 100 110 111 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ∈ 𝑇 )
113 1 3 10 11 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ∈ 𝐵 )
114 99 112 113 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ∈ 𝐵 )
115 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → 𝑆 ⊆ 𝐵 )
116 1 5 2 clatleglb ⊢ ( ( 𝐾 ∈ CLat ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) )
117 98 114 115 116 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) )
118 117 3expa ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ) → ( ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) )
119 118 pm5.32da ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ 𝑥 ) ) )
120 52 96 119 3bitr4rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ) )
121 opex ⊢ ⟨ 𝑓 , 𝑠 ⟩ ∈ V
122 eliin ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ V → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ) )
123 121 122 ax-mp ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) )
124 120 123 bitr4di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ◡ ( 𝑠 ‘ 𝐹 ) ) ) ≤ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
125 49 124 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
126 125 exp44 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝑞 ∈ 𝐴 → ( ¬ 𝑞 ≤ 𝑊 → ( ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
127 126 imp4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝑞 ∈ 𝐴 → ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) ) ) )
128 127 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( ( 𝐺 ‘ 𝑆 ) ∧ 𝑊 ) ) = ( 𝐺 ‘ 𝑆 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) ) )
129 41 128 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
130 129 eqrelrdv2 ⊢ ( ( ( Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) ∧ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
131 15 30 31 130 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) ∧ ¬ ( 𝐺 ‘ 𝑆 ) ≤ 𝑊 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )