Metamath Proof Explorer

Theorem diaglbN

Description: Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 diaglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
2 diaglb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 diaglb.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
6 5 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝐾 ∈ CLat )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 7 8 2 3 diadm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
10 9 sseq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ⊆ dom 𝐼 ↔ 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ) )
11 10 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ⊆ dom 𝐼 ) → 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
12 11 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } )
13 ssrab2 ⊢ { 𝑦 ∈ ( Base ‘ 𝐾 ) ∣ 𝑦 ( le ‘ 𝐾 ) 𝑊 } ⊆ ( Base ‘ 𝐾 )
14 12 13 sstrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
15 7 1 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
16 6 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → 𝑆 ≠ ∅ )
18 n0 ⊢ ( 𝑆 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑆 )
19 17 18 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ∃ 𝑥 𝑥 ∈ 𝑆 )
20 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
21 20 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ Lat )
22 16 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
23 ssel2 ⊢ ( ( 𝑆 ⊆ dom 𝐼 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ dom 𝐼 )
24 23 adantlr ⊢ ( ( ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ dom 𝐼 )
25 24 adantll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ dom 𝐼 )
26 7 8 2 3 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ dom 𝐼 ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) )
27 26 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ dom 𝐼 ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) )
28 25 27 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) )
29 28 simpld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
30 7 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
31 30 ad3antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
32 5 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐾 ∈ CLat )
33 14 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
34 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
35 7 8 1 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 )
36 32 33 34 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 )
37 28 simprd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ( le ‘ 𝐾 ) 𝑊 )
38 7 8 21 22 29 31 36 37 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 )
39 19 38 exlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 )
40 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
41 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
42 7 8 2 40 41 3 diaelval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) )
43 4 16 39 42 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) )
44 r19.28zv ⊢ ( 𝑆 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
45 44 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
46 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
47 7 8 2 40 41 3 diaelval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
48 46 28 47 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
49 48 ralbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
50 5 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐾 ∈ CLat )
51 7 2 40 41 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) )
52 51 adantlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) )
53 14 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
54 7 8 1 clatleglb ⊢ ( ( 𝐾 ∈ CLat ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) )
55 50 52 53 54 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) )
56 55 pm5.32da ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ↔ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
57 45 49 56 3bitr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) ) )
58 vex ⊢ 𝑓 ∈ V
59 eliin ⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) ) )
60 58 59 ax-mp ⊢ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 𝑓 ∈ ( 𝐼 ‘ 𝑥 ) )
61 57 60 bitr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ↔ 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
62 43 61 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) ↔ 𝑓 ∈ ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ) )
63 62 eqrdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅ ) ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) )