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 syl5bb ( ( ( 𝐾 ∈ 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 𝐼𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺𝑆 ) ) = 𝑥𝑆 ( 𝐼𝑥 ) )