Theorem cdleme50trn2 40660

Description: Part of proof that 𝐹 is a translation. Remove 𝑆 hypotheses no longer needed from cdleme50trn2a 40659. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Hypotheses

Ref	Expression
cdlemef50.b	⊢ 𝐵 = (Base‘𝐾)
cdlemef50.l	⊢ ≤ = (le‘𝐾)
cdlemef50.j	⊢ ∨ = (join‘𝐾)
cdlemef50.m	⊢ ∧ = (meet‘𝐾)
cdlemef50.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemef50.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemef50.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdlemef50.d	⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
cdlemefs50.e	⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
cdlemef50.f	⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))

Assertion

Ref	Expression
cdleme50trn2	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)

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

Allowed substitution hints:   𝐷(𝑡)   𝐸(𝑡,𝑠)   𝐹(𝑥,𝑦,𝑧,𝑡,𝑠)

Proof of Theorem cdleme50trn2

Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp11 1204	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp12 1205	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
3		simp13 1206	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
4		simp2l 1200	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄)
5		cdlemef50.l	. . . 4 ⊢ ≤ = (le‘𝐾)
6		cdlemef50.j	. . . 4 ⊢ ∨ = (join‘𝐾)
7		cdlemef50.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
8		cdlemef50.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
9	5, 6, 7, 8	cdlemb2 40150	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ∃𝑒 ∈ 𝐴 (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)))
10	1, 2, 3, 4, 9	syl121anc 1377	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ∃𝑒 ∈ 𝐴 (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)))
11		simp1 1136	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
12		simp2l 1200	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → 𝑃 ≠ 𝑄)
13		simp2r 1201	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
14		simp3rl 1247	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → 𝑒 ∈ 𝐴)
15		simprrl 780	. . . . . . . . . 10 ⊢ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑒 ≤ 𝑊)
16	15	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → ¬ 𝑒 ≤ 𝑊)
17	14, 16	jca 511	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → (𝑒 ∈ 𝐴 ∧ ¬ 𝑒 ≤ 𝑊))
18		simp3l 1202	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
19		simprrr 781	. . . . . . . . 9 ⊢ ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)))) → ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))
20	19	3ad2ant3 1135	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))
21		cdlemef50.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐾)
22		cdlemef50.m	. . . . . . . . 9 ⊢ ∧ = (meet‘𝐾)
23		cdlemef50.u	. . . . . . . . 9 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
24		cdlemef50.d	. . . . . . . . 9 ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
25		cdlemefs50.e	. . . . . . . . 9 ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
26		cdlemef50.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))
27	21, 5, 6, 22, 7, 8, 23, 24, 25, 26	cdleme50trn2a 40659	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑒 ∈ 𝐴 ∧ ¬ 𝑒 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
28	11, 12, 13, 17, 18, 20, 27	syl132anc 1390	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)
29	28	3exp 1119	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ((𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)))
30	29	exp4a 431	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑅 ≤ (𝑃 ∨ 𝑄) → ((𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈))))
31	30	3imp 1110	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑒 ∈ 𝐴 ∧ (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈))
32	31	expd 415	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑒 ∈ 𝐴 → ((¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)))
33	32	rexlimdv 3131	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (∃𝑒 ∈ 𝐴 (¬ 𝑒 ≤ 𝑊 ∧ ¬ 𝑒 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈))
34	10, 33	mpd 15	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ (𝐹‘𝑅)) ∧ 𝑊) = 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  ⦋csb 3845  ifcif 4472   class class class wbr 5089   ↦ cmpt 5170  ‘cfv 6481  ℩crio 7302  (class class class)co 7346  Basecbs 17120  lecple 17168  joincjn 18217  meetcmee 18218  Atomscatm 39372  HLchlt 39459  LHypclh 40093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-riotaBAD 39062

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-iin 4942  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-undef 8203  df-proset 18200  df-poset 18219  df-plt 18234  df-lub 18250  df-glb 18251  df-join 18252  df-meet 18253  df-p0 18329  df-p1 18330  df-lat 18338  df-clat 18405  df-oposet 39285  df-ol 39287  df-oml 39288  df-covers 39375  df-ats 39376  df-atl 39407  df-cvlat 39431  df-hlat 39460  df-llines 39607  df-lplanes 39608  df-lvols 39609  df-lines 39610  df-psubsp 39612  df-pmap 39613  df-padd 39905  df-lhyp 40097

This theorem is referenced by:  cdleme50trn12  40661