Theorem cdlemefs32sn1aw 40874

Description: Show that ⦋𝑅 / 𝑠⦌𝑁 is an atom not under 𝑊 when 𝑅 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 24-Mar-2013.)

Hypotheses

Ref	Expression
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

Ref	Expression
cdlemefs32sn1aw	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊))

Distinct variable groups:   𝑡,𝑠,𝑦,𝐴   𝐵,𝑠,𝑡,𝑦   𝑦,𝐷   𝑦,𝐸   𝐻,𝑠,𝑡,𝑦   ∨ ,𝑠,𝑡,𝑦   𝐾,𝑠,𝑡,𝑦   ≤ ,𝑠,𝑡,𝑦   ∧ ,𝑠,𝑡,𝑦   𝑃,𝑠,𝑡,𝑦   𝑄,𝑠,𝑡,𝑦   𝑅,𝑠,𝑡,𝑦   𝑡,𝑈,𝑦   𝑊,𝑠,𝑡,𝑦   𝑦,𝑌   𝐷,𝑠

Allowed substitution hints:   𝐶(𝑦,𝑡,𝑠)   𝐷(𝑡)   𝑈(𝑠)   𝐸(𝑡,𝑠)   𝐼(𝑦,𝑡,𝑠)   𝑁(𝑦,𝑡,𝑠)   𝑌(𝑡,𝑠)   𝑍(𝑦,𝑡,𝑠)

Proof of Theorem cdlemefs32sn1aw

Step	Hyp	Ref	Expression
1		cdlemefs32.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2	1	fvexi 6848	. . 3 ⊢ 𝐵 ∈ V
3		nfv 1916	. . . 4 ⊢ Ⅎ𝑡(((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))
4		cdlemefs32a1.z	. . . . . . . 8 ⊢ 𝑍 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌))
5		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)
6		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑡𝐵
7	5, 6	nfriota 7329	. . . . . . . 8 ⊢ Ⅎ𝑡(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌))
8	4, 7	nfcxfr 2897	. . . . . . 7 ⊢ Ⅎ𝑡𝑍
9	8	nfel1 2916	. . . . . 6 ⊢ Ⅎ𝑡 𝑍 ∈ 𝐴
10		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑡 ≤
11		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑡𝑊
12	8, 10, 11	nfbr 5133	. . . . . . 7 ⊢ Ⅎ𝑡 𝑍 ≤ 𝑊
13	12	nfn 1859	. . . . . 6 ⊢ Ⅎ𝑡 ¬ 𝑍 ≤ 𝑊
14	9, 13	nfan 1901	. . . . 5 ⊢ Ⅎ𝑡(𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊)
15	14	a1i 11	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → Ⅎ𝑡(𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊))
16	4	a1i 11	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑍 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝑌)))
17		eleq1 2825	. . . . . 6 ⊢ (𝑌 = 𝑍 → (𝑌 ∈ 𝐴 ↔ 𝑍 ∈ 𝐴))
18		breq1 5089	. . . . . . 7 ⊢ (𝑌 = 𝑍 → (𝑌 ≤ 𝑊 ↔ 𝑍 ≤ 𝑊))
19	18	notbid 318	. . . . . 6 ⊢ (𝑌 = 𝑍 → (¬ 𝑌 ≤ 𝑊 ↔ ¬ 𝑍 ≤ 𝑊))
20	17, 19	anbi12d 633	. . . . 5 ⊢ (𝑌 = 𝑍 → ((𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ≤ 𝑊) ↔ (𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊)))
21	20	adantl 481	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ 𝑌 = 𝑍) → ((𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ≤ 𝑊) ↔ (𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊)))
22		simpl1 1193	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
23		simpl2r 1229	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
24		simprl 771	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → 𝑡 ∈ 𝐴)
25		simprrl 781	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑡 ≤ 𝑊)
26	24, 25	jca 511	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊))
27		simpl2l 1228	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → 𝑃 ≠ 𝑄)
28		simpl3 1195	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
29		simprrr 782	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
30		cdlemefs32.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
31		cdlemefs32.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
32		cdlemefs32.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
33		cdlemefs32.a	. . . . . . . 8 ⊢ 𝐴 = (Atoms‘𝐾)
34		cdlemefs32.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
35		cdlemefs32.u	. . . . . . . 8 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
36		cdlemefs32.d	. . . . . . . 8 ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
37		cdlemefs32a1.y	. . . . . . . 8 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑅 ∨ 𝑡) ∧ 𝑊)))
38	30, 31, 32, 33, 34, 35, 36, 37	cdleme7ga 40708	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))) → 𝑌 ∈ 𝐴)
39	30, 31, 32, 33, 34, 35, 36, 37	cdleme7 40709	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑌 ≤ 𝑊)
40	38, 39	jca 511	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))) → (𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ≤ 𝑊))
41	22, 23, 26, 27, 28, 29, 40	syl123anc 1390	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))) → (𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ≤ 𝑊))
42	41	ex 412	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑡 ∈ 𝐴 ∧ (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))) → (𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ≤ 𝑊)))
43		simp1 1137	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
44		simp2rl 1244	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ∈ 𝐴)
45		simp2rr 1245	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑅 ≤ 𝑊)
46		simp2l 1201	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
47		simp3 1139	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≤ (𝑃 ∨ 𝑄))
48	1, 30, 31, 32, 33, 34, 35, 36, 37, 4	cdleme25cl 40817	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑍 ∈ 𝐵)
49	43, 44, 45, 46, 47, 48	syl122anc 1382	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑍 ∈ 𝐵)
50		simp11 1205	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
51		simp12 1206	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
52		simp13 1207	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
53	30, 31, 33, 34	cdlemb2 40501	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ∃𝑡 ∈ 𝐴 (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))
54	50, 51, 52, 46, 53	syl121anc 1378	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ∃𝑡 ∈ 𝐴 (¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)))
55	3, 15, 16, 21, 42, 49, 54	riotasv3d 39420	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ 𝐵 ∈ V) → (𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊))
56	2, 55	mpan2 692	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊))
57		cdlemefs32.e	. . . . . 6 ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
58		cdlemefs32.i	. . . . . 6 ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸))
59		cdlemefs32.n	. . . . . 6 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶)
60	57, 58, 59, 37, 4	cdleme31sn1c 40848	. . . . 5 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑍)
61	44, 47, 60	syl2anc 585	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑍)
62	61	eleq1d 2822	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ↔ 𝑍 ∈ 𝐴))
63	61	breq1d 5096	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊 ↔ 𝑍 ≤ 𝑊))
64	63	notbid 318	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊 ↔ ¬ 𝑍 ≤ 𝑊))
65	62, 64	anbi12d 633	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊) ↔ (𝑍 ∈ 𝐴 ∧ ¬ 𝑍 ≤ 𝑊)))
66	56, 65	mpbird 257	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (⦋𝑅 / 𝑠⦌𝑁 ∈ 𝐴 ∧ ¬ ⦋𝑅 / 𝑠⦌𝑁 ≤ 𝑊))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3430  ⦋csb 3838  ifcif 4467   class class class wbr 5086  ‘cfv 6492  ℩crio 7316  (class class class)co 7360  Basecbs 17170  lecple 17218  joincjn 18268  meetcmee 18269  Atomscatm 39723  HLchlt 39810  LHypclh 40444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-riotaBAD 39413

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-undef 8216  df-proset 18251  df-poset 18270  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-p1 18381  df-lat 18389  df-clat 18456  df-oposet 39636  df-ol 39638  df-oml 39639  df-covers 39726  df-ats 39727  df-atl 39758  df-cvlat 39782  df-hlat 39811  df-llines 39958  df-lplanes 39959  df-lvols 39960  df-lines 39961  df-psubsp 39963  df-pmap 39964  df-padd 40256  df-lhyp 40448

This theorem is referenced by:  cdlemefs32snb  40875  cdleme32sn1awN  40892  cdleme32snaw  40895