Metamath Proof Explorer

Theorem trlord

Description: The ordering of two Hilbert lattice elements (under the fiducial hyperplane W ) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014)

Ref Expression
Hypotheses trlord.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
trlord.l ⊢ ≤ = ( le ‘ 𝐾 )
trlord.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trlord.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trlord.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trlord.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trlord ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 trlord.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 trlord.l ⊢ ≤ = ( le ‘ 𝐾 )
3 trlord.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 trlord.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 trlord.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 trlord.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
9 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝑓 ∈ 𝑇 )
11 1 4 5 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 )
12 9 10 11 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 )
13 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
14 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝑌 ∈ 𝐵 )
15 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 )
16 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → 𝑋 ≤ 𝑌 )
17 1 2 8 12 13 14 15 16 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 )
18 17 exp44 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑓 ∈ 𝑇 → ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ) ) )
19 18 ralrimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 → ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ) )
20 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝐾 ∈ HL )
21 20 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝐾 ∈ Lat )
22 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑢 ∈ 𝐴 )
23 1 3 atbase ⊢ ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵 )
24 22 23 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑢 ∈ 𝐵 )
25 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
26 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑊 ∈ 𝐻 )
27 1 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
28 26 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑊 ∈ 𝐵 )
29 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑢 ≤ 𝑋 )
30 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑋 ≤ 𝑊 )
31 1 2 21 24 25 28 29 30 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → 𝑢 ≤ 𝑊 )
32 31 29 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑋 ) → ( 𝑢 ≤ 𝑊 ∧ 𝑢 ≤ 𝑋 ) )
33 32 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑢 ≤ 𝑋 → ( 𝑢 ≤ 𝑊 ∧ 𝑢 ≤ 𝑋 ) ) )
34 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ∈ 𝐴 )
36 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ≤ 𝑊 )
37 2 3 4 5 6 cdlemf ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) ) → ∃ 𝑔 ∈ 𝑇 ( 𝑅 ‘ 𝑔 ) = 𝑢 )
38 34 35 36 37 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ∃ 𝑔 ∈ 𝑇 ( 𝑅 ‘ 𝑔 ) = 𝑢 )
39 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) )
40 fveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑅 ‘ 𝑓 ) = ( 𝑅 ‘ 𝑔 ) )
41 40 breq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ↔ ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ) )
42 40 breq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ↔ ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) )
43 41 42 imbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ↔ ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) ) )
44 43 rspccv ⊢ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) → ( 𝑔 ∈ 𝑇 → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) ) )
45 39 44 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ( 𝑔 ∈ 𝑇 → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) ) )
46 breq1 ⊢ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 ↔ 𝑢 ≤ 𝑋 ) )
47 breq1 ⊢ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ↔ 𝑢 ≤ 𝑌 ) )
48 46 47 imbi12d ⊢ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) ↔ ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
49 48 biimpcd ⊢ ( ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑔 ) ≤ 𝑌 ) → ( ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
50 45 49 syl6 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ( 𝑔 ∈ 𝑇 → ( ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) ) )
51 50 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ( ∃ 𝑔 ∈ 𝑇 ( 𝑅 ‘ 𝑔 ) = 𝑢 → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
52 38 51 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑢 ≤ 𝑊 ) → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) )
53 52 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑢 ≤ 𝑊 → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
54 53 impd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ) → ( ( 𝑢 ≤ 𝑊 ∧ 𝑢 ≤ 𝑋 ) → 𝑢 ≤ 𝑌 ) )
55 33 54 syld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) )
56 55 exp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) → ( 𝑢 ∈ 𝐴 → ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) ) )
57 56 ralrimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) → ∀ 𝑢 ∈ 𝐴 ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
58 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
59 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
60 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
61 1 2 3 hlatle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑢 ∈ 𝐴 ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
62 58 59 60 61 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑢 ∈ 𝐴 ( 𝑢 ≤ 𝑋 → 𝑢 ≤ 𝑌 ) ) )
63 57 62 sylibrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) )
64 19 63 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ) )