Theorem 2llnmat 35322

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 1235	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ HL)
2		hlatl 35158	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
3	1, 2	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ AtLat)
4	1	hllatd 35162	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ Lat)
5		simpl2 1237	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ 𝑁)
6		eqid 2817	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		2llnmat.n	. . . . . . 7 ⊢ 𝑁 = (LLines‘𝐾)
8	6, 7	llnbase 35307	. . . . . 6 ⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝐾))
9	5, 8	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ (Base‘𝐾))
10		simpl3 1239	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ 𝑁)
11	6, 7	llnbase 35307	. . . . . 6 ⊢ (𝑌 ∈ 𝑁 → 𝑌 ∈ (Base‘𝐾))
12	10, 11	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ (Base‘𝐾))
13		2llnmat.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
14	6, 13	latmcl 17276	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
15	4, 9, 12, 14	syl3anc 1483	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
16		simprr 780	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ≠ 0 )
17		eqid 2817	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
18		2llnmat.z	. . . . 5 ⊢ 0 = (0.‘𝐾)
19		2llnmat.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
20	6, 17, 18, 19	atlex 35114	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ≠ 0 ) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
21	3, 15, 16, 20	syl3anc 1483	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
22		simp1rl 1312	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ≠ 𝑌)
23		simp1l 1247	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁))
24	17, 7	llncmp 35320	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
26		simp1l1 1358	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ HL)
27	26	hllatd 35162	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Lat)
28		simp1l2 1359	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ 𝑁)
29	28, 8	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ (Base‘𝐾))
30		simp1l3 1360	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ 𝑁)
31	30, 11	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ (Base‘𝐾))
32	6, 17, 13	latleeqm1 17303	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
33	27, 29, 31, 32	syl3anc 1483	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
34	25, 33	bitr3d 272	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 = 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
35	34	necon3bid 3033	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ≠ 𝑌 ↔ (𝑋 ∧ 𝑌) ≠ 𝑋))
36	22, 35	mpbid 223	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 𝑋)
37		simp3 1161	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
38	6, 17, 13	latmle1 17300	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
39	27, 29, 31, 38	syl3anc 1483	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
40		hlpos 35164	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	26, 40	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Poset)
42	6, 19	atbase 35087	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
43	42	3ad2ant2 1157	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ (Base‘𝐾))
44	27, 29, 31, 14	syl3anc 1483	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
45		simp2 1160	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ 𝐴)
46	6, 17, 27, 43, 44, 29, 37, 39	lattrd 17282	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)𝑋)
47		eqid 2817	. . . . . . . . . . . 12 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
48	17, 47, 19, 7	atcvrlln2 35317	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝( ⋖ ‘𝐾)𝑋)
49	26, 45, 28, 46, 48	syl31anc 1485	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝( ⋖ ‘𝐾)𝑋)
50	6, 17, 47	cvrnbtwn4 35077	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾)) ∧ 𝑝( ⋖ ‘𝐾)𝑋) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
51	41, 43, 29, 44, 49, 50	syl131anc 1495	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
52	37, 39, 51	mpbi2and 694	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋))
53		neor 3080	. . . . . . . 8 ⊢ ((𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋) ↔ (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
54	52, 53	sylib 209	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
55	54	necon1d 3011	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑋 ∧ 𝑌) ≠ 𝑋 → 𝑝 = (𝑋 ∧ 𝑌)))
56	36, 55	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 = (𝑋 ∧ 𝑌))
57	56	3exp 1141	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑝 ∈ 𝐴 → (𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → 𝑝 = (𝑋 ∧ 𝑌))))
58	57	reximdvai 3213	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌)))
59	21, 58	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
60		risset 3261	. 2 ⊢ ((𝑋 ∧ 𝑌) ∈ 𝐴 ↔ ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
61	59, 60	sylibr 225	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 865   ∧ w3a 1100   = wceq 1637   ∈ wcel 2157   ≠ wne 2989  ∃wrex 3108   class class class wbr 4855  ‘cfv 6110  (class class class)co 6883  Basecbs 16087  lecple 16179  Posetcpo 17164  meetcmee 17169  0.cp0 17261  Latclat 17269   ⋖ ccvr 35060  Atomscatm 35061  AtLatcal 35062  HLchlt 35148  LLinesclln 35289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-riota 6844  df-ov 6886  df-oprab 6887  df-proset 17152  df-poset 17170  df-plt 17182  df-lub 17198  df-glb 17199  df-join 17200  df-meet 17201  df-p0 17263  df-lat 17270  df-clat 17332  df-oposet 34974  df-ol 34976  df-oml 34977  df-covers 35064  df-ats 35065  df-atl 35096  df-cvlat 35120  df-hlat 35149  df-llines 35296

This theorem is referenced by:  2at0mat0  35323  ps-2c  35326  2llnmeqat  35369  dalemcea  35458  dalem2  35459  dalem21  35492  dalem54  35524  cdlemc5  35993