Metamath Proof Explorer


Theorem cdlemk26b-3

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 14-Jul-2013)

Ref Expression
Hypotheses cdlemk3.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk3.l = ( le ‘ 𝐾 )
cdlemk3.j = ( join ‘ 𝐾 )
cdlemk3.m = ( meet ‘ 𝐾 )
cdlemk3.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk3.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk3.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk3.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk3.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
cdlemk3.u1 𝑌 = ( 𝑑𝑇 , 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑑 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑑 ) ) ) ) ) )
Assertion cdlemk26b-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ∃ 𝑥𝑇 ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 cdlemk3.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk3.l = ( le ‘ 𝐾 )
3 cdlemk3.j = ( join ‘ 𝐾 )
4 cdlemk3.m = ( meet ‘ 𝐾 )
5 cdlemk3.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk3.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk3.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk3.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk3.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
10 cdlemk3.u1 𝑌 = ( 𝑑𝑇 , 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑑 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑑 ) ) ) ) ) )
11 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 1 6 7 8 cdlemftr2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑥𝑇 ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) )
13 11 12 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ∃ 𝑥𝑇 ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) )
14 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) )
15 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
16 simp133 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
17 simp131 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐺𝑇 )
18 simp121 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐹𝑇 )
19 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑥𝑇 )
20 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑁𝑇 )
21 simp3r2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) )
22 simp3r3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) )
23 21 22 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) )
24 simp122 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
25 simp132 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
26 simp3r1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑥 ≠ ( I ↾ 𝐵 ) )
27 24 25 26 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝑥 ≠ ( I ↾ 𝐵 ) ) )
28 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
29 1 2 3 4 5 6 7 8 9 10 cdlemkuel-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝑥𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝑥 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 )
30 15 16 17 18 19 20 23 27 28 29 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 )
31 14 30 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) )
32 31 3expia ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑥𝑇 ∧ ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ) → ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) ) )
33 32 expd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑥𝑇 → ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) → ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) ) ) )
34 33 reximdvai ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ∃ 𝑥𝑇 ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) → ∃ 𝑥𝑇 ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) ) )
35 13 34 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ∃ 𝑥𝑇 ( ( 𝑥 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑥 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑥 𝑌 𝐺 ) ∈ 𝑇 ) )