Metamath Proof Explorer


Theorem dihord2pre

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

Ref Expression
Hypotheses dihjust.b 𝐵 = ( Base ‘ 𝐾 )
dihjust.l = ( le ‘ 𝐾 )
dihjust.j = ( join ‘ 𝐾 )
dihjust.m = ( meet ‘ 𝐾 )
dihjust.a 𝐴 = ( Atoms ‘ 𝐾 )
dihjust.h 𝐻 = ( LHyp ‘ 𝐾 )
dihjust.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihjust.J 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dihjust.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjust.s = ( LSSum ‘ 𝑈 )
dihord2c.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihord2c.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihord2c.o 𝑂 = ( 𝑇 ↦ ( I ↾ 𝐵 ) )
dihord2.p 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihord2.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihord2.d + = ( +g𝑈 )
dihord2.g 𝐺 = ( 𝑇 ( 𝑃 ) = 𝑁 )
Assertion dihord2pre ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) )

Proof

Step Hyp Ref Expression
1 dihjust.b 𝐵 = ( Base ‘ 𝐾 )
2 dihjust.l = ( le ‘ 𝐾 )
3 dihjust.j = ( join ‘ 𝐾 )
4 dihjust.m = ( meet ‘ 𝐾 )
5 dihjust.a 𝐴 = ( Atoms ‘ 𝐾 )
6 dihjust.h 𝐻 = ( LHyp ‘ 𝐾 )
7 dihjust.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8 dihjust.J 𝐽 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
9 dihjust.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
10 dihjust.s = ( LSSum ‘ 𝑈 )
11 dihord2c.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
12 dihord2c.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 dihord2c.o 𝑂 = ( 𝑇 ↦ ( I ↾ 𝐵 ) )
14 dihord2.p 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
15 dihord2.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
16 dihord2.d + = ( +g𝑈 )
17 dihord2.g 𝐺 = ( 𝑇 ( 𝑃 ) = 𝑁 )
18 simpl1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) )
19 simpl2l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝑋𝐵 )
20 simpl2r ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝑌𝐵 )
21 simpl3 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) )
22 simprl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝑓𝑇 )
23 simprr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑅𝑓 ) ( 𝑋 𝑊 ) )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 dihord11c ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ∧ 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ∃ 𝑦 ∈ ( 𝐽𝑁 ) ∃ 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) )
25 18 19 20 21 22 23 24 syl123anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ∃ 𝑦 ∈ ( 𝐽𝑁 ) ∃ 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) )
26 simpl11 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
27 simpl13 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) )
28 2 5 6 14 11 15 8 17 dicelval3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) → ( 𝑦 ∈ ( 𝐽𝑁 ) ↔ ∃ 𝑠𝐸 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ) )
29 26 27 28 syl2anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑦 ∈ ( 𝐽𝑁 ) ↔ ∃ 𝑠𝐸 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ) )
30 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝐾 ∈ HL )
31 30 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝐾 ∈ HL )
32 31 hllatd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝐾 ∈ Lat )
33 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝑊𝐻 )
34 33 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝑊𝐻 )
35 1 6 lhpbase ( 𝑊𝐻𝑊𝐵 )
36 34 35 syl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → 𝑊𝐵 )
37 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵 ) → ( 𝑌 𝑊 ) ∈ 𝐵 )
38 32 20 36 37 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑌 𝑊 ) ∈ 𝐵 )
39 1 2 4 latmle2 ( ( 𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵 ) → ( 𝑌 𝑊 ) 𝑊 )
40 32 20 36 39 syl3anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑌 𝑊 ) 𝑊 )
41 1 2 6 11 12 13 7 dibelval3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑌 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 𝑊 ) 𝑊 ) ) → ( 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ↔ ∃ 𝑔𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) )
42 26 38 40 41 syl12anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ↔ ∃ 𝑔𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) )
43 29 42 anbi12d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝑦 ∈ ( 𝐽𝑁 ) ∧ 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ↔ ( ∃ 𝑠𝐸 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ∃ 𝑔𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) ) )
44 reeanv ( ∃ 𝑠𝐸𝑔𝑇 ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) ↔ ( ∃ 𝑠𝐸 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ∃ 𝑔𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) )
45 simpll1 ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) ∧ ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) )
46 simplr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) ∧ ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) )
47 simpr ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) ∧ ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) )
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 dihord10 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ∧ ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) )
49 45 46 47 48 syl3anc ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) ∧ ( ( 𝑠𝐸𝑔𝑇 ) ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ∧ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) )
50 49 3exp2 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝑠𝐸𝑔𝑇 ) → ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ) )
51 oveq12 ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( 𝑦 + 𝑧 ) = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) )
52 51 eqeq2d ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) ↔ ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) ) )
53 52 imbi1d ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ↔ ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
54 53 imbi2d ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ↔ ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ) )
55 54 biimprd ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) → ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ) )
56 55 com23 ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ) → ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ) )
57 56 impr ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) → ( ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
58 57 com12 ( ( ( 𝑅𝑔 ) ( 𝑌 𝑊 ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( ⟨ ( 𝑠𝐺 ) , 𝑠+𝑔 , 𝑂 ⟩ ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) → ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
59 50 58 syl6 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝑠𝐸𝑔𝑇 ) → ( ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) ) )
60 59 rexlimdvv ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ∃ 𝑠𝐸𝑔𝑇 ( 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
61 44 60 syl5bir ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( ∃ 𝑠𝐸 𝑦 = ⟨ ( 𝑠𝐺 ) , 𝑠 ⟩ ∧ ∃ 𝑔𝑇 ( 𝑧 = ⟨ 𝑔 , 𝑂 ⟩ ∧ ( 𝑅𝑔 ) ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
62 43 61 sylbid ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ( 𝑦 ∈ ( 𝐽𝑁 ) ∧ 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) → ( ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
63 62 rexlimdvv ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( ∃ 𝑦 ∈ ( 𝐽𝑁 ) ∃ 𝑧 ∈ ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ⟨ 𝑓 , 𝑂 ⟩ = ( 𝑦 + 𝑧 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) )
64 25 63 mpd ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) ∧ ( 𝑓𝑇 ∧ ( 𝑅𝑓 ) ( 𝑋 𝑊 ) ) ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) )
65 64 exp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑓𝑇 → ( ( 𝑅𝑓 ) ( 𝑋 𝑊 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
66 65 ralrimiv ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ∀ 𝑓𝑇 ( ( 𝑅𝑓 ) ( 𝑋 𝑊 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) )
67 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
68 30 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝐾 ∈ Lat )
69 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝑋𝐵 )
70 33 35 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝑊𝐵 )
71 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
72 68 69 70 71 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
73 1 2 4 latmle2 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) 𝑊 )
74 68 69 70 73 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑋 𝑊 ) 𝑊 )
75 simp2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → 𝑌𝐵 )
76 68 75 70 37 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑌 𝑊 ) ∈ 𝐵 )
77 68 75 70 39 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑌 𝑊 ) 𝑊 )
78 1 2 5 6 11 12 trlord ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 𝑊 ) 𝑊 ) ∧ ( ( 𝑌 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 𝑊 ) 𝑊 ) ) → ( ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) ↔ ∀ 𝑓𝑇 ( ( 𝑅𝑓 ) ( 𝑋 𝑊 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
79 67 72 74 76 77 78 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) ↔ ∀ 𝑓𝑇 ( ( 𝑅𝑓 ) ( 𝑋 𝑊 ) → ( 𝑅𝑓 ) ( 𝑌 𝑊 ) ) ) )
80 66 79 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑁𝐴 ∧ ¬ 𝑁 𝑊 ) ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝐽𝑄 ) ( 𝐼 ‘ ( 𝑋 𝑊 ) ) ) ⊆ ( ( 𝐽𝑁 ) ( 𝐼 ‘ ( 𝑌 𝑊 ) ) ) ) → ( 𝑋 𝑊 ) ( 𝑌 𝑊 ) )