Metamath Proof Explorer

Theorem cdlemg8b

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013)

Ref Expression
Hypotheses cdlemg8.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemg8.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemg8.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemg8.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg8.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg8b ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( 𝑃 ∨ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 cdlemg8.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemg8.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemg8.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdlemg8.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemg8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemg8.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝐾 ∈ HL )
8 7 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝐾 ∈ Lat )
9 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑃 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
12 9 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13 simp22l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑄 ∈ 𝐴 )
14 10 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
16 10 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
17 8 12 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
18 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝐹 ∈ 𝑇 )
20 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝐺 ∈ 𝑇 )
21 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
22 1 4 5 6 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
23 18 20 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
24 1 4 5 6 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ 𝑊 ) )
25 24 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 )
26 18 19 23 25 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 )
27 10 4 atbase ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
28 26 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
29 10 5 6 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30 18 20 15 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐺 ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
31 10 5 6 ltrncl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝐺 ‘ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
32 18 19 30 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
33 10 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) )
34 8 28 32 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) )
35 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) )
36 34 35 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
37 10 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
38 7 9 13 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
39 10 1 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
40 8 12 28 38 39 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) ) )
41 17 36 40 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
42 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 )
43 42 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → 𝑃 ≠ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) )
44 1 2 4 ps-1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∈ 𝐴 ∧ 𝑃 ≠ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( 𝑃 ∨ 𝑄 ) ) )
45 7 9 26 43 9 13 44 syl132anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( 𝑃 ∨ 𝑄 ) ) )
46 41 45 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ) = ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ≠ 𝑃 ) ) → ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) = ( 𝑃 ∨ 𝑄 ) )