Metamath Proof Explorer

Theorem cdlemg7fvbwN

Description: Properties of a translation of an element not under W . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw ? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg4.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemg4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion cdlemg7fvbwN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdlemg4.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemg4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 cdlemg4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 cdlemg4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemg4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
6 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
8 5 1 6 7 2 3 lhpmcvr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
9 8 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) )
10 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑟 ∈ 𝐴 )
12 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ¬ 𝑟 ≤ 𝑊 )
13 11 12 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) )
14 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
15 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐹 ∈ 𝑇 )
16 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 )
17 3 4 1 6 2 7 5 cdlemg2fv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) )
18 10 13 14 15 16 17 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) )
19 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
20 19 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
21 1 2 3 4 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 ) )
22 21 simpld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 )
23 10 15 13 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 )
24 5 2 atbase ⊢ ( ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 → ( 𝐹 ‘ 𝑟 ) ∈ 𝐵 )
25 23 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐵 )
26 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
27 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
28 5 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
29 27 28 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
30 5 7 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 )
31 20 26 29 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 )
32 5 6 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑟 ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ 𝐵 )
33 20 25 31 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ 𝐵 )
34 18 33 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
35 21 simprd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ) → ¬ ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 )
36 10 15 13 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 )
37 5 1 6 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑟 ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑟 ) ≤ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) )
38 20 25 31 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐹 ‘ 𝑟 ) ≤ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) )
39 5 1 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ 𝑟 ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑟 ) ≤ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ≤ 𝑊 ) → ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 ) )
40 20 25 33 29 39 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑟 ) ≤ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ≤ 𝑊 ) → ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 ) )
41 38 40 mpand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ≤ 𝑊 → ( 𝐹 ‘ 𝑟 ) ≤ 𝑊 ) )
42 36 41 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ¬ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ≤ 𝑊 )
43 18 breq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ↔ ( ( 𝐹 ‘ 𝑟 ) ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ≤ 𝑊 ) )
44 42 43 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 )
45 34 44 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑟 ∈ 𝐴 ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) )
46 45 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) ) )
47 9 46 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝑋 ) ≤ 𝑊 ) )