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

Metamath Proof Explorer

Theorem dihord6apre

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord6apre.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihord6apre.l ⊢ ≤ = ( le ‘ 𝐾 )
dihord6apre.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihord6apre.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihord6apre.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihord6apre.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihord6apre.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihord6apre.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihord6apre.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihord6apre.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihord6apre.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihord6apre.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
Assertion dihord6apre ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) → 𝑋 ≤ 𝑌 )

Proof

Step Hyp Ref Expression
1 dihord6apre.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihord6apre.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihord6apre.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 dihord6apre.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 dihord6apre.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
6 dihord6apre.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7 dihord6apre.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 dihord6apre.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
9 dihord6apre.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
10 dihord6apre.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
11 dihord6apre.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
12 dihord6apre.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
13 1 4 7 8 6 tendo1ne0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 𝑂 )
14 13 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ≠ 𝑂 )
15 14 neneqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ ( I ↾ 𝑇 ) = 𝑂 )
16 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
17 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
18 1 2 16 17 3 4 lhpmcvr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
19 18 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
20 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
22 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
23 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
24 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
25 1 2 16 17 3 4 9 23 24 10 11 dihvalcq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
26 20 21 22 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
27 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
28 1 2 4 9 23 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) )
29 20 27 28 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) )
30 26 29 sseq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) )
31 4 10 20 dvhlmod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑈 ∈ LMod )
32 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
33 32 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
34 31 33 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
35 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
36 2 3 4 10 24 32 diclss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( LSubSp ‘ 𝑈 ) )
37 20 35 36 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( LSubSp ‘ 𝑈 ) )
38 34 37 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝑈 ) )
39 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
40 39 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
41 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
42 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
43 1 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
44 42 43 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
45 1 17 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 )
46 40 41 44 45 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 )
47 1 2 17 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
48 40 41 44 47 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
49 1 2 4 10 23 32 diblss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
50 20 46 48 49 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
51 34 50 sseldd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
52 11 lsmub1 ⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
53 38 51 52 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
54 sstr ⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) → ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) )
55 eqidd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) )
56 4 7 8 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
57 20 56 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
58 fvex ⊢ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ V
59 7 fvexi ⊢ 𝑇 ∈ V
60 resiexg ⊢ ( 𝑇 ∈ V → ( I ↾ 𝑇 ) ∈ V )
61 59 60 ax-mp ⊢ ( I ↾ 𝑇 ) ∈ V
62 2 3 4 5 7 8 24 12 58 61 dicopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) )
63 20 35 62 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) = ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) )
64 55 57 63 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) )
65 ssel2 ⊢ ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ) → ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) )
66 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
67 1 2 4 7 6 66 23 dibopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) ) )
68 20 27 67 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ↔ ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) ) )
69 simpr ⊢ ( ( ( ( I ↾ 𝑇 ) ‘ 𝐺 ) ∈ ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → ( I ↾ 𝑇 ) = 𝑂 )
70 68 69 biimtrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) )
71 65 70 syl5 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ∧ ⟨ ( ( I ↾ 𝑇 ) ‘ 𝐺 ) , ( I ↾ 𝑇 ) ⟩ ∈ ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ) → ( I ↾ 𝑇 ) = 𝑂 ) )
72 64 71 mpan2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) )
73 54 72 syl5 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) → ( I ↾ 𝑇 ) = 𝑂 ) )
74 53 73 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ⊕ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) )
75 30 74 sylbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) )
76 75 exp44 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ¬ 𝑞 ≤ 𝑊 → ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) ) ) )
77 76 imp4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) ) )
78 77 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) ) )
79 19 78 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → ( I ↾ 𝑇 ) = 𝑂 ) )
80 15 79 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ¬ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) )
81 80 pm2.21d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) → 𝑋 ≤ 𝑌 ) )
82 81 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ) → 𝑋 ≤ 𝑌 )