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

Metamath Proof Explorer

Theorem dihmeetlem2N

Description: Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetlem2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem2.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeetlem2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem2.l ⊢ ≤ = ( le ‘ 𝐾 )
dihmeetlem2.j ⊢ ∨ = ( join ‘ 𝐾 )
dihmeetlem2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihmeetlem2.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem2.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihmeetlem2.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
dihmeetlem2.o ⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion dihmeetlem2N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dihmeetlem2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem2.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 dihmeetlem2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihmeetlem2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dihmeetlem2.l ⊢ ≤ = ( le ‘ 𝐾 )
6 dihmeetlem2.j ⊢ ∨ = ( join ‘ 𝐾 )
7 dihmeetlem2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 dihmeetlem2.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
9 dihmeetlem2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10 dihmeetlem2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11 dihmeetlem2.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12 dihmeetlem2.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
13 dihmeetlem2.o ⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
14 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
15 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
16 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
17 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
18 14 2 15 16 17 meetval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
19 18 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) )
20 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
22 1 5 3 21 dibeldmN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )
23 22 biimpar ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) )
24 23 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) )
25 1 5 3 21 dibeldmN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑌 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) )
26 25 biimpar ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) )
27 26 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) )
28 prssg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑌 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ { 𝑋 , 𝑌 } ⊆ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ) )
29 16 17 28 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝑋 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑌 ∈ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ { 𝑋 , 𝑌 } ⊆ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ) )
30 24 27 29 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → { 𝑋 , 𝑌 } ⊆ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) )
31 prnzg ⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 , 𝑌 } ≠ ∅ )
32 16 31 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → { 𝑋 , 𝑌 } ≠ ∅ )
33 14 3 21 dibglbN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( { 𝑋 , 𝑌 } ⊆ dom ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ∧ { 𝑋 , 𝑌 } ≠ ∅ ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
34 20 30 32 33 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
35 19 34 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∧ 𝑌 ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
36 15 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
37 1 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
38 36 16 17 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
39 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
40 1 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
41 39 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐵 )
42 1 5 2 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
43 36 16 17 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
44 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ≤ 𝑊 )
45 1 5 36 38 16 41 43 44 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
46 1 5 3 4 21 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∧ 𝑌 ) ) )
47 20 38 45 46 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∧ 𝑌 ) ) )
48 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 ∈ { 𝑋 , 𝑌 } ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 vex ⊢ 𝑥 ∈ V
50 49 elpr ⊢ ( 𝑥 ∈ { 𝑋 , 𝑌 } ↔ ( 𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ) )
51 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
52 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
53 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊 ) )
54 52 53 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )
55 54 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )
56 51 55 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
57 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑌 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
58 eleq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵 ) )
59 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ≤ 𝑊 ↔ 𝑌 ≤ 𝑊 ) )
60 58 59 anbi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) )
61 60 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑌 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) )
62 57 61 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑌 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
63 56 62 jaodan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
64 50 63 sylan2b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 ∈ { 𝑋 , 𝑌 } ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) )
65 1 5 3 4 21 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑥 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
66 48 64 65 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ 𝑥 ∈ { 𝑋 , 𝑌 } ) → ( 𝐼 ‘ 𝑥 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
67 66 iineq2dv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
68 35 47 67 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) )
69 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑋 ) )
70 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑌 ) )
71 69 70 iinxprg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
72 16 17 71 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ∩ 𝑥 ∈ { 𝑋 , 𝑌 } ( 𝐼 ‘ 𝑥 ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
73 68 72 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )