Theorem dihmeetlem3N 39013

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
dihmeetlem3.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem3.l	⊢ ≤ = (le‘𝐾)
dihmeetlem3.j	⊢ ∨ = (join‘𝐾)
dihmeetlem3.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem3.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem3.h	⊢ 𝐻 = (LHyp‘𝐾)

Assertion

Ref	Expression
dihmeetlem3N	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑄 ≠ 𝑅)

Proof of Theorem dihmeetlem3N

Step	Hyp	Ref	Expression
1		simp2lr 1243	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → ¬ 𝑄 ≤ 𝑊)
2		oveq1 7209	. . . . . . 7 ⊢ (𝑄 = 𝑅 → (𝑄 ∨ (𝑌 ∧ 𝑊)) = (𝑅 ∨ (𝑌 ∧ 𝑊)))
3		simpr 488	. . . . . . 7 ⊢ (((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)
4	2, 3	sylan9eqr 2796	. . . . . 6 ⊢ ((((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) ∧ 𝑄 = 𝑅) → (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌)
5		dihmeetlem3.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
6		dihmeetlem3.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
7		simp11l 1286	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝐾 ∈ HL)
8	7	hllatd 37072	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝐾 ∈ Lat)
9		simp2ll 1242	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ∈ 𝐴)
10		dihmeetlem3.a	. . . . . . . . . 10 ⊢ 𝐴 = (Atoms‘𝐾)
11	5, 10	atbase 36997	. . . . . . . . 9 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
12	9, 11	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ∈ 𝐵)
13		simp12l 1288	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑋 ∈ 𝐵)
14		simp12r 1289	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑌 ∈ 𝐵)
15		dihmeetlem3.m	. . . . . . . . . 10 ⊢ ∧ = (meet‘𝐾)
16	5, 15	latmcl 17918	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
17	8, 13, 14, 16	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑌) ∈ 𝐵)
18		simp11r 1287	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑊 ∈ 𝐻)
19		dihmeetlem3.h	. . . . . . . . . 10 ⊢ 𝐻 = (LHyp‘𝐾)
20	5, 19	lhpbase 37706	. . . . . . . . 9 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
21	18, 20	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑊 ∈ 𝐵)
22	5, 15	latmcl 17918	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
23	8, 13, 21, 22	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑊) ∈ 𝐵)
24		dihmeetlem3.j	. . . . . . . . . . . 12 ⊢ ∨ = (join‘𝐾)
25	5, 6, 24	latlej1 17926	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊)))
26	8, 12, 23, 25	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊)))
27		simp2r 1202	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
28	26, 27	breqtrd 5069	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑋)
29	5, 15	latmcl 17918	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵)
30	8, 14, 21, 29	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑌 ∧ 𝑊) ∈ 𝐵)
31	5, 6, 24	latlej1 17926	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ∈ 𝐵) → 𝑄 ≤ (𝑄 ∨ (𝑌 ∧ 𝑊)))
32	8, 12, 30, 31	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑄 ∨ (𝑌 ∧ 𝑊)))
33		simp3 1140	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌)
34	32, 33	breqtrd 5069	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑌)
35	5, 6, 15	latlem12 17944	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑄 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ↔ 𝑄 ≤ (𝑋 ∧ 𝑌)))
36	8, 12, 13, 14, 35	syl13anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → ((𝑄 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ↔ 𝑄 ≤ (𝑋 ∧ 𝑌)))
37	28, 34, 36	mpbi2and 712	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ (𝑋 ∧ 𝑌))
38		simp13 1207	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑋 ∧ 𝑌) ≤ 𝑊)
39	5, 6, 8, 12, 17, 21, 37, 38	lattrd 17924	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ (𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → 𝑄 ≤ 𝑊)
40	39	3exp 1121	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → ((𝑄 ∨ (𝑌 ∧ 𝑊)) = 𝑌 → 𝑄 ≤ 𝑊)))
41	4, 40	syl7 74	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → ((((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) ∧ 𝑄 = 𝑅) → 𝑄 ≤ 𝑊)))
42	41	exp4a 435	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) → (((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) → (𝑄 = 𝑅 → 𝑄 ≤ 𝑊))))
43	42	3imp 1113	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (𝑄 = 𝑅 → 𝑄 ≤ 𝑊))
44	43	necon3bd 2949	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → (¬ 𝑄 ≤ 𝑊 → 𝑄 ≠ 𝑅))
45	1, 44	mpd 15	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑄 ≠ 𝑅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110   ≠ wne 2935   class class class wbr 5043  ‘cfv 6369  (class class class)co 7202  Basecbs 16684  lecple 16774  joincjn 17790  meetcmee 17791  Latclat 17909  Atomscatm 36971  HLchlt 37058  LHypclh 37692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-poset 17792  df-lub 17824  df-glb 17825  df-join 17826  df-meet 17827  df-lat 17910  df-ats 36975  df-atl 37006  df-cvlat 37030  df-hlat 37059  df-lhyp 37696

This theorem is referenced by: (None)