Theorem cdleme48bw 41296

Description: TODO: fix comment. TODO: Remove unnecessary 𝑃 ≠ 𝑄 from cdleme48bw 41296 cdlemeg46c 41307 cdlemeg46fvaw 41310 cdlemeg46rgv 41322 cdlemeg46gfv 41324? cdleme48d 41329? and possibly others they affect. (Contributed by NM, 9-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
cdleme48bw	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ (𝐹‘𝑋) ≤ 𝑊)

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

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

Proof of Theorem cdleme48bw

Step	Hyp	Ref	Expression
1		simp1 1154	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
2		simp3l 1220	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))
3		cdlemef46.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
4		cdlemef46.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
5		cdlemef46.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
6		cdlemef46.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
7		cdlemef46.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
8		cdlemef46.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
9		cdlemef46.u	. . . . 5 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
10		cdlemef46.d	. . . . 5 ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
11		cdlemefs46.e	. . . . 5 ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
12		cdlemef46.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))), 𝑥))
13	3, 4, 5, 6, 7, 8, 9, 10, 11, 12	cdleme46fvaw 41295	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝐹‘𝑆) ∈ 𝐴 ∧ ¬ (𝐹‘𝑆) ≤ 𝑊))
14	1, 2, 13	syl2anc 595	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝐹‘𝑆) ∈ 𝐴 ∧ ¬ (𝐹‘𝑆) ≤ 𝑊))
15	14	simprd 500	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ (𝐹‘𝑆) ≤ 𝑊)
16		simp11l 1303	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
17	16	hllatd 40158	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
18	14	simpld 499	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑆) ∈ 𝐴)
19	3, 7	atbase 40083	. . . . . 6 ⊢ ((𝐹‘𝑆) ∈ 𝐴 → (𝐹‘𝑆) ∈ 𝐵)
20	18, 19	syl 18	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑆) ∈ 𝐵)
21		simp2rl 1261	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
22		simp11r 1304	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
23	3, 8	lhpbase 40792	. . . . . . 7 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
24	22, 23	syl 18	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
25	3, 6	latmcl 18491	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
26	17, 21, 24, 25	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	3, 4, 5	latlej1 18499	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑆) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (𝐹‘𝑆) ≤ ((𝐹‘𝑆) ∨ (𝑋 ∧ 𝑊)))
28	17, 20, 26, 27	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑆) ≤ ((𝐹‘𝑆) ∨ (𝑋 ∧ 𝑊)))
29	3, 4, 5, 6, 7, 8, 9, 10, 11, 12	cdleme48fv 41293	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) = ((𝐹‘𝑆) ∨ (𝑋 ∧ 𝑊)))
30	28, 29	breqtrrd 5139	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑆) ≤ (𝐹‘𝑋))
31		vex 3459	. . . . . . 7 ⊢ 𝑠 ∈ V
32		eqid 2763	. . . . . . . 8 ⊢ ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
33	10, 32	cdleme31sc 41178	. . . . . . 7 ⊢ (𝑠 ∈ V → ⦋𝑠 / 𝑡⦌𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))))
34	31, 33	ax-mp 5	. . . . . 6 ⊢ ⦋𝑠 / 𝑡⦌𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
35		eqid 2763	. . . . . 6 ⊢ (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)) = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸))
36		eqid 2763	. . . . . 6 ⊢ if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) = if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷)
37		eqid 2763	. . . . . 6 ⊢ (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊)))) = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (if(𝑠 ≤ (𝑃 ∨ 𝑄), (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸)), ⦋𝑠 / 𝑡⦌𝐷) ∨ (𝑥 ∧ 𝑊))))
38	3, 4, 5, 6, 7, 8, 9, 34, 10, 11, 35, 36, 37, 12	cdleme32fvcl 41234	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵)
39	1, 21, 38	syl2anc 595	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐹‘𝑋) ∈ 𝐵)
40	3, 4	lattr 18495	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑆) ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐹‘𝑆) ≤ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≤ 𝑊) → (𝐹‘𝑆) ≤ 𝑊))
41	17, 20, 39, 24, 40	syl13anc 1399	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝐹‘𝑆) ≤ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≤ 𝑊) → (𝐹‘𝑆) ≤ 𝑊))
42	30, 41	mpand 707	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝐹‘𝑋) ≤ 𝑊 → (𝐹‘𝑆) ≤ 𝑊))
43	15, 42	mtod 201	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ (𝐹‘𝑋) ≤ 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  Vcvv 3455  ⦋csb 3853  ifcif 4487   class class class wbr 5109   ↦ cmpt 5192  ‘cfv 6536  ℩crio 7366  (class class class)co 7410  Basecbs 17264  lecple 17312  joincjn 18362  meetcmee 18363  Latclat 18482  Atomscatm 40057  HLchlt 40144  LHypclh 40778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-riotaBAD 39747

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-undef 8265  df-proset 18345  df-poset 18364  df-plt 18379  df-lub 18395  df-glb 18396  df-join 18397  df-meet 18398  df-p0 18474  df-p1 18475  df-lat 18483  df-clat 18550  df-oposet 39970  df-ol 39972  df-oml 39973  df-covers 40060  df-ats 40061  df-atl 40092  df-cvlat 40116  df-hlat 40145  df-llines 40292  df-lplanes 40293  df-lvols 40294  df-lines 40295  df-psubsp 40297  df-pmap 40298  df-padd 40590  df-lhyp 40782

This theorem is referenced by:  cdleme48d  41329