Metamath Proof Explorer


Theorem cdlemk28-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 cdlemk28-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 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → 𝐹𝑇 )
13 simp21r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
14 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → 𝑁𝑇 )
15 12 13 14 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) )
16 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → 𝐺𝑇 )
17 simp22r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
18 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
19 16 17 18 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
20 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
21 1 2 3 4 5 6 7 8 9 10 cdlemk26b-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑁𝑇 ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ∃ 𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑏 𝑌 𝐺 ) ∈ 𝑇 ) )
22 11 15 19 20 21 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ∃ 𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑏 𝑌 𝐺 ) ∈ 𝑇 ) )
23 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
24 12 3ad2ant1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐹𝑇 )
25 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑏𝑇 )
26 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑁𝑇 )
27 24 25 26 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐹𝑇𝑏𝑇𝑁𝑇 ) )
28 16 3ad2ant1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐺𝑇 )
29 simp2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑎𝑇 )
30 28 29 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐺𝑇𝑎𝑇 ) )
31 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
32 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
33 13 3ad2ant1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
34 simp3l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑏 ≠ ( I ↾ 𝐵 ) )
35 32 33 34 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑏 ≠ ( I ↾ 𝐵 ) ) )
36 17 3ad2ant1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
37 simp3r1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝑎 ≠ ( I ↾ 𝐵 ) )
38 36 37 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝑎 ≠ ( I ↾ 𝐵 ) ) )
39 simp3r3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) )
40 39 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝑎 ) )
41 simp3r2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) )
42 simp3l2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) )
43 40 41 42 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( ( 𝑅𝐺 ) ≠ ( 𝑅𝑎 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ) )
44 simp3l3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) )
45 44 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝑏 ) )
46 1 2 3 4 5 6 7 8 9 10 cdlemk27-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝑏𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝑎𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑏 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝑎 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝑎 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑏 ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) )
47 23 27 30 31 35 38 43 45 46 syl332anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) ∧ ( 𝑏𝑇𝑎𝑇 ) ∧ ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) )
48 47 3exp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ( ( 𝑏𝑇𝑎𝑇 ) → ( ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) ) ) )
49 48 ralrimivv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ∀ 𝑏𝑇𝑎𝑇 ( ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) ) )
50 neeq1 ( 𝑏 = 𝑎 → ( 𝑏 ≠ ( I ↾ 𝐵 ) ↔ 𝑎 ≠ ( I ↾ 𝐵 ) ) )
51 fveq2 ( 𝑏 = 𝑎 → ( 𝑅𝑏 ) = ( 𝑅𝑎 ) )
52 51 neeq1d ( 𝑏 = 𝑎 → ( ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ↔ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ) )
53 51 neeq1d ( 𝑏 = 𝑎 → ( ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ↔ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) )
54 50 52 53 3anbi123d ( 𝑏 = 𝑎 → ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ↔ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) )
55 oveq1 ( 𝑏 = 𝑎 → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) )
56 54 55 reusv3 ( ∃ 𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑏 𝑌 𝐺 ) ∈ 𝑇 ) → ( ∀ 𝑏𝑇𝑎𝑇 ( ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) ) ↔ ∃ 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → 𝑧 = ( 𝑏 𝑌 𝐺 ) ) ) )
57 56 biimpd ( ∃ 𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑏 𝑌 𝐺 ) ∈ 𝑇 ) → ( ∀ 𝑏𝑇𝑎𝑇 ( ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝑎 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑎 ) ≠ ( 𝑅𝐺 ) ) ) → ( 𝑏 𝑌 𝐺 ) = ( 𝑎 𝑌 𝐺 ) ) → ∃ 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → 𝑧 = ( 𝑏 𝑌 𝐺 ) ) ) )
58 22 49 57 sylc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝑁𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ) → ∃ 𝑧𝑇𝑏𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) → 𝑧 = ( 𝑏 𝑌 𝐺 ) ) )