This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dibglbN

Description: Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
dibglb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dibglb.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibglbN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dibglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
2 dibglb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dibglb.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
4 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ dom 𝐼 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 6 7 2 3 dibdmN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
9 8 sseq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ⊆ dom 𝐼 ↔ 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ) )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝑆 ⊆ dom 𝐼 ↔ 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ) )
11 5 10 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
12 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
13 2 3 dibvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) )
15 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
16 15 biimpi ⊢ ( 𝑆 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝑆 )
17 16 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑥 𝑥 ∈ 𝑆 )
18 2 3 dibvalrel ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑥 ) )
19 18 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → Rel ( 𝐼 ‘ 𝑥 ) )
20 19 a1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝑥 ∈ 𝑆 → Rel ( 𝐼 ‘ 𝑥 ) ) )
21 20 ancld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) ) )
22 21 eximdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ∃ 𝑥 𝑥 ∈ 𝑆 → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) ) )
23 17 22 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) )
24 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ Rel ( 𝐼 ‘ 𝑥 ) ) )
25 23 24 sylibr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) )
26 reliin ⊢ ( ∃ 𝑥 ∈ 𝑆 Rel ( 𝐼 ‘ 𝑥 ) → Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
27 25 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
28 id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) )
29 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
31 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
32 6 7 2 31 diadm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
33 32 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
34 30 33 sseqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
35 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
36 1 2 31 diaglbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑆 ≠ ∅ ) ) → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
37 29 34 35 36 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
38 37 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
39 vex ⊢ 𝑓 ∈ V
40 eliin ⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
41 39 40 ax-mp ⊢ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
42 38 41 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
43 42 anbi1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
44 r19.27zv ⊢ ( 𝑆 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
45 44 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
46 43 45 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
47 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
48 47 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → 𝐾 ∈ CLat )
49 ssrab2 ⊢ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ⊆ ( Base ‘ 𝐾 )
50 30 49 sstrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
51 6 1 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
52 48 50 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
53 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
54 53 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ Lat )
55 47 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ CLat )
56 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
57 56 49 sstrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
58 55 57 51 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
59 50 sselda ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
60 6 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
61 60 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
62 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
63 6 7 1 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 )
64 55 57 62 63 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 )
65 30 sselda ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
66 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( le ‘ 𝐾 ) 𝑊 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
67 66 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
68 65 67 sylib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
69 68 simprd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ( le ‘ 𝐾 ) 𝑊 )
70 6 7 54 58 59 61 64 69 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 )
71 17 70 exlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 )
72 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
73 eqid ⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
74 6 7 2 72 73 31 3 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
75 29 52 71 74 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
76 opex ⊢ ⟨ 𝑓 , 𝑠 ⟩ ∈ V
77 eliin ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ V → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ) )
78 76 77 ax-mp ⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) )
79 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
80 6 7 2 72 73 31 3 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
81 79 68 80 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
82 81 ralbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝑆 ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
83 78 82 bitrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∧ 𝑠 = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) ) )
84 46 75 83 3bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ⟨ 𝑓 , 𝑠 ⟩ ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
85 84 eqrelrdv2 ⊢ ( ( ( Rel ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ∧ Rel ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) ∧ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
86 14 27 28 85 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )
87 4 11 12 86 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )