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

Metamath Proof Explorer

Theorem cdleme48bw

Description: TODO: fix comment. TODO: Remove unnecessary P =/= Q from cdleme48bw cdlemeg46c cdlemeg46fvaw cdlemeg46rgv cdlemeg46gfv ? cdleme48d ? and possibly others they affect. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef46.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemef46.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemef46.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemef46.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdlemef46.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemef46.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemef46.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdlemef46.d ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
cdlemefs46.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
cdlemef46.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) , 𝑥 ) )
Assertion cdleme48bw ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 )

Proof

Step Hyp Ref Expression
1 cdlemef46.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemef46.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemef46.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cdlemef46.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cdlemef46.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemef46.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemef46.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8 cdlemef46.d ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
9 cdlemefs46.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
10 cdlemef46.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) , 𝑥 ) )
11 simp1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
12 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
13 1 2 3 4 5 6 7 8 9 10 cdleme46fvaw ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑆 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 ) )
14 11 12 13 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐹 ‘ 𝑆 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 ) )
15 14 simprd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 )
16 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
17 16 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
18 14 simpld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑆 ) ∈ 𝐴 )
19 1 5 atbase ⊢ ( ( 𝐹 ‘ 𝑆 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑆 ) ∈ 𝐵 )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑆 ) ∈ 𝐵 )
21 simp2rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
22 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
23 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
24 22 23 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
25 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
26 17 21 24 25 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
27 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐹 ‘ 𝑆 ) ∨ ( 𝑋 ∧ 𝑊 ) ) )
28 17 20 26 27 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐹 ‘ 𝑆 ) ∨ ( 𝑋 ∧ 𝑊 ) ) )
29 1 2 3 4 5 6 7 8 9 10 cdleme48fv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑆 ) ∨ ( 𝑋 ∧ 𝑊 ) ) )
30 28 29 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑆 ) ≤ ( 𝐹 ‘ 𝑋 ) )
31 vex ⊢ 𝑠 ∈ V
32 eqid ⊢ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
33 8 32 cdleme31sc ⊢ ( 𝑠 ∈ V → ⦋ 𝑠 / 𝑡 ⦌ 𝐷 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) )
34 31 33 ax-mp ⊢ ⦋ 𝑠 / 𝑡 ⦌ 𝐷 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
35 eqid ⊢ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) )
36 eqid ⊢ if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 )
37 eqid ⊢ ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
38 1 2 3 4 5 6 7 34 8 9 35 36 37 10 cdleme32fvcl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
39 11 21 38 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
40 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑆 ) ≤ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) → ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 ) )
41 17 20 39 24 40 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑆 ) ≤ ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) → ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 ) )
42 30 41 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 → ( 𝐹 ‘ 𝑆 ) ≤ 𝑊 ) )
43 15 42 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑆 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 )