Metamath Proof Explorer

Theorem dihord4

Description: The isomorphism H for a lattice K is order-preserving in the region not under co-atom W . TODO: reformat ( q e. A /\ -. q .<_ W ) to eliminate adant*. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihord3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihord3.l ⊢ ≤ = ( le ‘ 𝐾 )
dihord3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihord3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihord4 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dihord3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihord3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihord3.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dihord3.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 1 2 5 6 7 3 lhpmcvr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
9 8 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
10 1 2 5 6 7 3 lhpmcvr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) )
11 10 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) )
12 reeanv ⊢ ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ↔ ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) )
13 9 11 12 sylanbrc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) )
14 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
16 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
17 simp3ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ¬ 𝑞 ≤ 𝑊 )
18 16 17 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) )
19 simp3lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 )
20 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
21 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
22 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
23 eqid ⊢ ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
24 1 2 5 6 7 3 4 20 21 22 23 dihvalcq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
25 14 15 18 19 24 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
26 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) )
27 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
28 simp3rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ¬ 𝑟 ≤ 𝑊 )
29 27 28 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) )
30 simp3rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 )
31 1 2 5 6 7 3 4 20 21 22 23 dihvalcq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ∧ ( ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
32 14 26 29 30 31 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
33 25 32 sseq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
34 simpl11 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 simpl2l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
36 17 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ¬ 𝑞 ≤ 𝑊 )
37 35 36 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) )
38 simpl2r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
39 28 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ¬ 𝑟 ≤ 𝑊 )
40 38 39 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) )
41 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
42 41 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑋 ∈ 𝐵 )
43 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑌 ∈ 𝐵 )
44 43 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑌 ∈ 𝐵 )
45 19 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 )
46 30 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 )
47 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
48 1 2 5 6 7 3 20 21 22 23 dihord2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) → 𝑋 ≤ 𝑌 )
49 34 37 40 42 44 45 46 47 48 syl323anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑋 ≤ 𝑌 )
50 simpl11 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
51 simpl2l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
52 17 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑞 ≤ 𝑊 )
53 51 52 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) )
54 simpl2r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
55 28 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑟 ≤ 𝑊 )
56 54 55 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) )
57 41 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 )
58 43 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝐵 )
59 19 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 )
60 30 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 )
61 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
62 1 2 5 6 7 3 20 21 22 23 dihord1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
63 50 53 56 57 58 59 60 61 62 syl323anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
64 49 63 impbida ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ↔ 𝑋 ≤ 𝑌 ) )
65 33 64 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) )
66 65 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) ) )
67 66 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) )
68 13 67 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) )