Metamath Proof Explorer


Theorem cdlemefs32sn1aw

Description: Show that [_ R / s ]_ N is an atom not under W when R .<_ ( P .\/ Q ) . (Contributed by NM, 24-Mar-2013)

Ref Expression
Hypotheses cdlemefs32.b 𝐵 = ( Base ‘ 𝐾 )
cdlemefs32.l = ( le ‘ 𝐾 )
cdlemefs32.j = ( join ‘ 𝐾 )
cdlemefs32.m = ( meet ‘ 𝐾 )
cdlemefs32.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemefs32.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemefs32.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdlemefs32.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdlemefs32.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdlemefs32.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐸 ) )
cdlemefs32.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
cdlemefs32a1.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑡 ) 𝑊 ) ) )
cdlemefs32a1.z 𝑍 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
Assertion cdlemefs32sn1aw ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑅 / 𝑠 𝑁𝐴 ∧ ¬ 𝑅 / 𝑠 𝑁 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdlemefs32.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemefs32.l = ( le ‘ 𝐾 )
3 cdlemefs32.j = ( join ‘ 𝐾 )
4 cdlemefs32.m = ( meet ‘ 𝐾 )
5 cdlemefs32.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemefs32.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemefs32.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdlemefs32.d 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
9 cdlemefs32.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
10 cdlemefs32.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐸 ) )
11 cdlemefs32.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐶 )
12 cdlemefs32a1.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑡 ) 𝑊 ) ) )
13 cdlemefs32a1.z 𝑍 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
14 1 fvexi 𝐵 ∈ V
15 nfv 𝑡 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) )
16 nfra1 𝑡𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 )
17 nfcv 𝑡 𝐵
18 16 17 nfriota 𝑡 ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
19 13 18 nfcxfr 𝑡 𝑍
20 19 nfel1 𝑡 𝑍𝐴
21 nfcv 𝑡
22 nfcv 𝑡 𝑊
23 19 21 22 nfbr 𝑡 𝑍 𝑊
24 23 nfn 𝑡 ¬ 𝑍 𝑊
25 20 24 nfan 𝑡 ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 )
26 25 a1i ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → Ⅎ 𝑡 ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) )
27 13 a1i ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑍 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) ) )
28 eleq1 ( 𝑌 = 𝑍 → ( 𝑌𝐴𝑍𝐴 ) )
29 breq1 ( 𝑌 = 𝑍 → ( 𝑌 𝑊𝑍 𝑊 ) )
30 29 notbid ( 𝑌 = 𝑍 → ( ¬ 𝑌 𝑊 ↔ ¬ 𝑍 𝑊 ) )
31 28 30 anbi12d ( 𝑌 = 𝑍 → ( ( 𝑌𝐴 ∧ ¬ 𝑌 𝑊 ) ↔ ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) ) )
32 31 adantl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝑌 = 𝑍 ) → ( ( 𝑌𝐴 ∧ ¬ 𝑌 𝑊 ) ↔ ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) ) )
33 simpl1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
34 simpl2r ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
35 simprl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → 𝑡𝐴 )
36 simprrl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑡 𝑊 )
37 35 36 jca ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) )
38 simpl2l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → 𝑃𝑄 )
39 simpl3 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
40 simprrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑡 ( 𝑃 𝑄 ) )
41 2 3 4 5 6 7 8 12 cdleme7ga ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) → 𝑌𝐴 )
42 2 3 4 5 6 7 8 12 cdleme7 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) → ¬ 𝑌 𝑊 )
43 41 42 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) → ( 𝑌𝐴 ∧ ¬ 𝑌 𝑊 ) )
44 33 34 37 38 39 40 43 syl123anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( 𝑌𝐴 ∧ ¬ 𝑌 𝑊 ) )
45 44 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) → ( 𝑌𝐴 ∧ ¬ 𝑌 𝑊 ) ) )
46 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
47 simp2rl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅𝐴 )
48 simp2rr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ¬ 𝑅 𝑊 )
49 simp2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑃𝑄 )
50 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 ( 𝑃 𝑄 ) )
51 1 2 3 4 5 6 7 8 12 13 cdleme25cl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝑍𝐵 )
52 46 47 48 49 50 51 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑍𝐵 )
53 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
54 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
55 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
56 2 3 5 6 cdlemb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ∃ 𝑡𝐴 ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) )
57 53 54 55 49 56 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ∃ 𝑡𝐴 ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) )
58 15 26 27 32 45 52 57 riotasv3d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ∧ 𝐵 ∈ V ) → ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) )
59 14 58 mpan2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) )
60 9 10 11 12 13 cdleme31sn1c ( ( 𝑅𝐴𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝑍 )
61 47 50 60 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝑍 )
62 61 eleq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑅 / 𝑠 𝑁𝐴𝑍𝐴 ) )
63 61 breq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑅 / 𝑠 𝑁 𝑊𝑍 𝑊 ) )
64 63 notbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( ¬ 𝑅 / 𝑠 𝑁 𝑊 ↔ ¬ 𝑍 𝑊 ) )
65 62 64 anbi12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( ( 𝑅 / 𝑠 𝑁𝐴 ∧ ¬ 𝑅 / 𝑠 𝑁 𝑊 ) ↔ ( 𝑍𝐴 ∧ ¬ 𝑍 𝑊 ) ) )
66 59 65 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑅 / 𝑠 𝑁𝐴 ∧ ¬ 𝑅 / 𝑠 𝑁 𝑊 ) )