Theorem 2llnmat 39929

Description: Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.)

Hypotheses

Ref	Expression
2llnmat.m	⊢ ∧ = (meet‘𝐾)
2llnmat.z	⊢ 0 = (0.‘𝐾)
2llnmat.a	⊢ 𝐴 = (Atoms‘𝐾)
2llnmat.n	⊢ 𝑁 = (LLines‘𝐾)

Assertion

Ref	Expression
2llnmat	⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)

Proof of Theorem 2llnmat

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1193	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ HL)
2		hlatl 39765	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
3	1, 2	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ AtLat)
4	1	hllatd 39769	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ Lat)
5		simpl2 1194	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ 𝑁)
6		eqid 2737	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		2llnmat.n	. . . . . . 7 ⊢ 𝑁 = (LLines‘𝐾)
8	6, 7	llnbase 39914	. . . . . 6 ⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝐾))
9	5, 8	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ (Base‘𝐾))
10		simpl3 1195	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ 𝑁)
11	6, 7	llnbase 39914	. . . . . 6 ⊢ (𝑌 ∈ 𝑁 → 𝑌 ∈ (Base‘𝐾))
12	10, 11	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ (Base‘𝐾))
13		2llnmat.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
14	6, 13	latmcl 18377	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
15	4, 9, 12, 14	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
16		simprr 773	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ≠ 0 )
17		eqid 2737	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
18		2llnmat.z	. . . . 5 ⊢ 0 = (0.‘𝐾)
19		2llnmat.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
20	6, 17, 18, 19	atlex 39721	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ≠ 0 ) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
21	3, 15, 16, 20	syl3anc 1374	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
22		simp1rl 1240	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ≠ 𝑌)
23		simp1l 1199	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁))
24	17, 7	llncmp 39927	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
26		simp1l1 1268	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ HL)
27	26	hllatd 39769	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Lat)
28		simp1l2 1269	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ 𝑁)
29	28, 8	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ (Base‘𝐾))
30		simp1l3 1270	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ 𝑁)
31	30, 11	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ (Base‘𝐾))
32	6, 17, 13	latleeqm1 18404	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
33	27, 29, 31, 32	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
34	25, 33	bitr3d 281	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 = 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
35	34	necon3bid 2977	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ≠ 𝑌 ↔ (𝑋 ∧ 𝑌) ≠ 𝑋))
36	22, 35	mpbid 232	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 𝑋)
37		simp3 1139	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
38	6, 17, 13	latmle1 18401	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
39	27, 29, 31, 38	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
40		hlpos 39771	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	26, 40	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Poset)
42	6, 19	atbase 39694	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
43	42	3ad2ant2 1135	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ (Base‘𝐾))
44	27, 29, 31, 14	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
45		simp2 1138	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ 𝐴)
46	6, 17, 27, 43, 44, 29, 37, 39	lattrd 18383	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)𝑋)
47		eqid 2737	. . . . . . . . . . . 12 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
48	17, 47, 19, 7	atcvrlln2 39924	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝( ⋖ ‘𝐾)𝑋)
49	26, 45, 28, 46, 48	syl31anc 1376	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝( ⋖ ‘𝐾)𝑋)
50	6, 17, 47	cvrnbtwn4 39684	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾)) ∧ 𝑝( ⋖ ‘𝐾)𝑋) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
51	41, 43, 29, 44, 49, 50	syl131anc 1386	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
52	37, 39, 51	mpbi2and 713	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋))
53		neor 3025	. . . . . . . 8 ⊢ ((𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋) ↔ (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
54	52, 53	sylib 218	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
55	54	necon1d 2955	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑋 ∧ 𝑌) ≠ 𝑋 → 𝑝 = (𝑋 ∧ 𝑌)))
56	36, 55	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 = (𝑋 ∧ 𝑌))
57	56	3exp 1120	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑝 ∈ 𝐴 → (𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → 𝑝 = (𝑋 ∧ 𝑌))))
58	57	reximdvai 3149	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌)))
59	21, 58	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
60		risset 3213	. 2 ⊢ ((𝑋 ∧ 𝑌) ∈ 𝐴 ↔ ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
61	59, 60	sylibr 234	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∃wrex 3062   class class class wbr 5100  ‘cfv 6502  (class class class)co 7370  Basecbs 17150  lecple 17198  Posetcpo 18244  meetcmee 18249  0.cp0 18358  Latclat 18368   ⋖ ccvr 39667  Atomscatm 39668  AtLatcal 39669  HLchlt 39755  LLinesclln 39896

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 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-proset 18231  df-poset 18250  df-plt 18265  df-lub 18281  df-glb 18282  df-join 18283  df-meet 18284  df-p0 18360  df-lat 18369  df-clat 18436  df-oposet 39581  df-ol 39583  df-oml 39584  df-covers 39671  df-ats 39672  df-atl 39703  df-cvlat 39727  df-hlat 39756  df-llines 39903

This theorem is referenced by:  2at0mat0  39930  ps-2c  39933  2llnmeqat  39976  dalemcea  40065  dalem2  40066  dalem21  40099  dalem54  40131  cdlemc5  40600