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

Metamath Proof Explorer

Theorem cdlemm10N

Description: The image of the map G is the entire one-dimensional subspace ( IV ) . Remark after Lemma M of Crawley p. 121 line 23. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemm10.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemm10.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemm10.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemm10.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemm10.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemm10.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemm10.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
cdlemm10.c ⊢ 𝐶 = { 𝑟 ∈ 𝐴 ∣ ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑟 ≤ 𝑊 ) }
cdlemm10.f ⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 )
cdlemm10.g ⊢ 𝐺 = ( 𝑞 ∈ 𝐶 ↦ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑞 ) )
Assertion cdlemm10N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ran 𝐺 = ( 𝐼 ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdlemm10.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemm10.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemm10.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemm10.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 cdlemm10.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 cdlemm10.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemm10.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemm10.c ⊢ 𝐶 = { 𝑟 ∈ 𝐴 ∣ ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑟 ≤ 𝑊 ) }
9 cdlemm10.f ⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 )
10 cdlemm10.g ⊢ 𝐺 = ( 𝑞 ∈ 𝐶 ↦ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑞 ) )
11 riotaex ⊢ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑞 ) ∈ V
12 11 10 fnmpti ⊢ 𝐺 Fn 𝐶
13 fvelrnb ⊢ ( 𝐺 Fn 𝐶 → ( 𝑔 ∈ ran 𝐺 ↔ ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 ) )
14 12 13 ax-mp ⊢ ( 𝑔 ∈ ran 𝐺 ↔ ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 )
15 eqeq2 ⊢ ( 𝑞 = 𝑠 → ( ( 𝑓 ‘ 𝑃 ) = 𝑞 ↔ ( 𝑓 ‘ 𝑃 ) = 𝑠 ) )
16 15 riotabidv ⊢ ( 𝑞 = 𝑠 → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑞 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 ) )
17 riotaex ⊢ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 ) ∈ V
18 16 10 17 fvmpt ⊢ ( 𝑠 ∈ 𝐶 → ( 𝐺 ‘ 𝑠 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 ) )
19 18 9 eqtr4di ⊢ ( 𝑠 ∈ 𝐶 → ( 𝐺 ‘ 𝑠 ) = 𝐹 )
20 19 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑠 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑠 ) = 𝐹 )
21 20 eqeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑠 ∈ 𝐶 ) → ( ( 𝐺 ‘ 𝑠 ) = 𝑔 ↔ 𝐹 = 𝑔 ) )
22 21 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 ↔ ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 ) )
23 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑔 ∈ 𝑇 )
25 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑃 ∈ 𝐴 )
26 1 3 4 5 ltrnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑃 ) ∈ 𝐴 )
27 23 24 25 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑔 ‘ 𝑃 ) ∈ 𝐴 )
28 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
29 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝐾 ∈ HL )
30 29 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝐾 ∈ Lat )
31 28 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 25 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
33 28 4 5 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑔 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
34 23 24 32 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑔 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
35 28 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑔 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
36 30 32 34 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
37 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑉 ∈ 𝐴 )
38 28 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
39 29 25 37 38 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
40 28 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑔 ‘ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) )
41 30 32 34 40 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) )
42 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
43 1 2 3 4 5 6 trljat1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) = ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) )
44 23 24 42 43 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) = ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) )
45 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 )
46 28 4 5 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑔 ) ∈ ( Base ‘ 𝐾 ) )
47 23 24 46 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑅 ‘ 𝑔 ) ∈ ( Base ‘ 𝐾 ) )
48 28 3 atbase ⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
49 37 48 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
50 28 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝑔 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ≤ ( 𝑃 ∨ 𝑉 ) ) )
51 30 47 49 32 50 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ≤ ( 𝑃 ∨ 𝑉 ) ) )
52 45 51 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝑔 ) ) ≤ ( 𝑃 ∨ 𝑉 ) )
53 44 52 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑃 ∨ ( 𝑔 ‘ 𝑃 ) ) ≤ ( 𝑃 ∨ 𝑉 ) )
54 28 1 30 34 36 39 41 53 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ 𝑉 ) )
55 1 3 4 5 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑔 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) )
56 55 simprd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 )
57 23 24 42 56 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 )
58 54 57 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) )
59 breq1 ⊢ ( 𝑟 = ( 𝑔 ‘ 𝑃 ) → ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ↔ ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ 𝑉 ) ) )
60 breq1 ⊢ ( 𝑟 = ( 𝑔 ‘ 𝑃 ) → ( 𝑟 ≤ 𝑊 ↔ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) )
61 60 notbid ⊢ ( 𝑟 = ( 𝑔 ‘ 𝑃 ) → ( ¬ 𝑟 ≤ 𝑊 ↔ ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) )
62 59 61 anbi12d ⊢ ( 𝑟 = ( 𝑔 ‘ 𝑃 ) → ( ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ( ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) ) )
63 62 8 elrab2 ⊢ ( ( 𝑔 ‘ 𝑃 ) ∈ 𝐶 ↔ ( ( 𝑔 ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝑔 ‘ 𝑃 ) ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ ( 𝑔 ‘ 𝑃 ) ≤ 𝑊 ) ) )
64 27 58 63 sylanbrc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( 𝑔 ‘ 𝑃 ) ∈ 𝐶 )
65 1 3 4 5 cdlemeiota ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑔 ∈ 𝑇 ) → 𝑔 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) )
66 23 42 24 65 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → 𝑔 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) )
67 66 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) = 𝑔 )
68 eqeq2 ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑃 ) → ( ( 𝑓 ‘ 𝑃 ) = 𝑠 ↔ ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) )
69 68 riotabidv ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑃 ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑠 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) )
70 9 69 eqtrid ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑃 ) → 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) )
71 70 eqeq1d ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑃 ) → ( 𝐹 = 𝑔 ↔ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) = 𝑔 ) )
72 71 rspcev ⊢ ( ( ( 𝑔 ‘ 𝑃 ) ∈ 𝐶 ∧ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = ( 𝑔 ‘ 𝑃 ) ) = 𝑔 ) → ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 )
73 64 67 72 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) → ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 )
74 73 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) → ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 ) )
75 breq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ↔ 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ) )
76 breq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ≤ 𝑊 ↔ 𝑠 ≤ 𝑊 ) )
77 76 notbid ⊢ ( 𝑟 = 𝑠 → ( ¬ 𝑟 ≤ 𝑊 ↔ ¬ 𝑠 ≤ 𝑊 ) )
78 75 77 anbi12d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑟 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ↔ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) )
79 78 8 elrab2 ⊢ ( 𝑠 ∈ 𝐶 ↔ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) )
80 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
81 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
82 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ¬ 𝑃 ≤ 𝑊 )
83 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑠 ∈ 𝐴 )
84 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ¬ 𝑠 ≤ 𝑊 )
85 1 3 4 5 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
86 1 3 4 5 9 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑠 )
87 85 86 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) )
88 80 81 82 83 84 87 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) )
89 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → 𝐹 ∈ 𝑇 )
90 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
91 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
92 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
93 1 2 92 3 4 5 6 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
94 90 89 91 93 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
95 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑠 )
96 95 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) = ( 𝑃 ∨ 𝑠 ) )
97 96 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) )
98 94 97 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) )
99 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
100 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑉 ∈ 𝐴 )
101 1 2 3 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑉 ) )
102 99 81 100 101 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑉 ) )
103 simprrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) )
104 99 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
105 81 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
106 28 3 atbase ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ( Base ‘ 𝐾 ) )
107 106 ad2antrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐾 ) )
108 99 81 100 38 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
109 28 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑉 ) ∧ 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ) ↔ ( 𝑃 ∨ 𝑠 ) ≤ ( 𝑃 ∨ 𝑉 ) ) )
110 104 105 107 108 109 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑉 ) ∧ 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ) ↔ ( 𝑃 ∨ 𝑠 ) ≤ ( 𝑃 ∨ 𝑉 ) ) )
111 102 103 110 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑠 ) ≤ ( 𝑃 ∨ 𝑉 ) )
112 28 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) )
113 99 81 83 112 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝑃 ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) )
114 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑊 ∈ 𝐻 )
115 28 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
116 114 115 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
117 28 1 92 latmlem1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑠 ) ≤ ( 𝑃 ∨ 𝑉 ) → ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ ( ( 𝑃 ∨ 𝑉 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
118 104 113 108 116 117 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑠 ) ≤ ( 𝑃 ∨ 𝑉 ) → ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ ( ( 𝑃 ∨ 𝑉 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
119 111 118 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ ( ( 𝑃 ∨ 𝑉 ) ( meet ‘ 𝐾 ) 𝑊 ) )
120 1 2 92 3 4 lhpat4N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑉 ) ( meet ‘ 𝐾 ) 𝑊 ) = 𝑉 )
121 120 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑉 ) ( meet ‘ 𝐾 ) 𝑊 ) = 𝑉 )
122 119 121 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑉 )
123 122 3adant3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( ( 𝑃 ∨ 𝑠 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑉 )
124 98 123 eqbrtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 )
125 89 124 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑠 ) ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) )
126 88 125 mpd3an3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≤ ( 𝑃 ∨ 𝑉 ) ∧ ¬ 𝑠 ≤ 𝑊 ) ) ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) )
127 79 126 sylan2b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑠 ∈ 𝐶 ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) )
128 127 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑠 ∈ 𝐶 → ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) ) )
129 eleq1 ⊢ ( 𝐹 = 𝑔 → ( 𝐹 ∈ 𝑇 ↔ 𝑔 ∈ 𝑇 ) )
130 fveq2 ⊢ ( 𝐹 = 𝑔 → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑔 ) )
131 130 breq1d ⊢ ( 𝐹 = 𝑔 → ( ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ↔ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) )
132 129 131 anbi12d ⊢ ( 𝐹 = 𝑔 → ( ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) )
133 132 biimpcd ⊢ ( ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑉 ) → ( 𝐹 = 𝑔 → ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) )
134 128 133 syl6 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑠 ∈ 𝐶 → ( 𝐹 = 𝑔 → ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) ) )
135 134 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 → ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) )
136 74 135 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ↔ ∃ 𝑠 ∈ 𝐶 𝐹 = 𝑔 ) )
137 22 136 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) ) )
138 fveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑅 ‘ 𝑓 ) = ( 𝑅 ‘ 𝑔 ) )
139 138 breq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 ↔ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) )
140 139 elrab ⊢ ( 𝑔 ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 } ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑔 ) ≤ 𝑉 ) )
141 137 140 bitr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 ↔ 𝑔 ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 } ) )
142 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
143 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
144 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ 𝐴 )
145 144 48 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
146 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ≤ 𝑊 )
147 28 1 4 5 6 7 diaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) = { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 } )
148 142 143 145 146 147 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) = { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 } )
149 148 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑔 ∈ ( 𝐼 ‘ 𝑉 ) ↔ 𝑔 ∈ { 𝑓 ∈ 𝑇 ∣ ( 𝑅 ‘ 𝑓 ) ≤ 𝑉 } ) )
150 141 149 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ∃ 𝑠 ∈ 𝐶 ( 𝐺 ‘ 𝑠 ) = 𝑔 ↔ 𝑔 ∈ ( 𝐼 ‘ 𝑉 ) ) )
151 14 150 bitrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑔 ∈ ran 𝐺 ↔ 𝑔 ∈ ( 𝐼 ‘ 𝑉 ) ) )
152 151 eqrdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ran 𝐺 = ( 𝐼 ‘ 𝑉 ) )