Theorem 2llnmat 36216

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 1184	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ HL)
2		hlatl 36052	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
3	1, 2	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ AtLat)
4	1	hllatd 36056	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝐾 ∈ Lat)
5		simpl2 1185	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ 𝑁)
6		eqid 2795	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		2llnmat.n	. . . . . . 7 ⊢ 𝑁 = (LLines‘𝐾)
8	6, 7	llnbase 36201	. . . . . 6 ⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝐾))
9	5, 8	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑋 ∈ (Base‘𝐾))
10		simpl3 1186	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ 𝑁)
11	6, 7	llnbase 36201	. . . . . 6 ⊢ (𝑌 ∈ 𝑁 → 𝑌 ∈ (Base‘𝐾))
12	10, 11	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → 𝑌 ∈ (Base‘𝐾))
13		2llnmat.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
14	6, 13	latmcl 17496	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
15	4, 9, 12, 14	syl3anc 1364	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
16		simprr 769	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ≠ 0 )
17		eqid 2795	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
18		2llnmat.z	. . . . 5 ⊢ 0 = (0.‘𝐾)
19		2llnmat.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
20	6, 17, 18, 19	atlex 36008	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ≠ 0 ) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
21	3, 15, 16, 20	syl3anc 1364	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
22		simp1rl 1231	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ≠ 𝑌)
23		simp1l 1190	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁))
24	17, 7	llncmp 36214	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ 𝑋 = 𝑌))
26		simp1l1 1259	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ HL)
27	26	hllatd 36056	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Lat)
28		simp1l2 1260	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ 𝑁)
29	28, 8	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑋 ∈ (Base‘𝐾))
30		simp1l3 1261	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ 𝑁)
31	30, 11	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑌 ∈ (Base‘𝐾))
32	6, 17, 13	latleeqm1 17523	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
33	27, 29, 31, 32	syl3anc 1364	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋(le‘𝐾)𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
34	25, 33	bitr3d 282	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 = 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
35	34	necon3bid 3028	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ≠ 𝑌 ↔ (𝑋 ∧ 𝑌) ≠ 𝑋))
36	22, 35	mpbid 233	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 𝑋)
37		simp3 1131	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)(𝑋 ∧ 𝑌))
38	6, 17, 13	latmle1 17520	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
39	27, 29, 31, 38	syl3anc 1364	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑋)
40		hlpos 36058	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	26, 40	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝐾 ∈ Poset)
42	6, 19	atbase 35981	. . . . . . . . . . 11 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
43	42	3ad2ant2 1127	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ (Base‘𝐾))
44	27, 29, 31, 14	syl3anc 1364	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾))
45		simp2 1130	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 ∈ 𝐴)
46	6, 17, 27, 43, 44, 29, 37, 39	lattrd 17502	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝(le‘𝐾)𝑋)
47		eqid 2795	. . . . . . . . . . . 12 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
48	17, 47, 19, 7	atcvrlln2 36211	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁) ∧ 𝑝(le‘𝐾)𝑋) → 𝑝( ⋖ ‘𝐾)𝑋)
49	26, 45, 28, 46, 48	syl31anc 1366	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝( ⋖ ‘𝐾)𝑋)
50	6, 17, 47	cvrnbtwn4 35971	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾)) ∧ 𝑝( ⋖ ‘𝐾)𝑋) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
51	41, 43, 29, 44, 49, 50	syl131anc 1376	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑝(le‘𝐾)(𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑋) ↔ (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋)))
52	37, 39, 51	mpbi2and 708	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋))
53		neor 3076	. . . . . . . 8 ⊢ ((𝑝 = (𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑌) = 𝑋) ↔ (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
54	52, 53	sylib 219	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → (𝑝 ≠ (𝑋 ∧ 𝑌) → (𝑋 ∧ 𝑌) = 𝑋))
55	54	necon1d 3006	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → ((𝑋 ∧ 𝑌) ≠ 𝑋 → 𝑝 = (𝑋 ∧ 𝑌)))
56	36, 55	mpd 15	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) ∧ 𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)(𝑋 ∧ 𝑌)) → 𝑝 = (𝑋 ∧ 𝑌))
57	56	3exp 1112	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑝 ∈ 𝐴 → (𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → 𝑝 = (𝑋 ∧ 𝑌))))
58	57	reximdvai 3235	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)(𝑋 ∧ 𝑌) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌)))
59	21, 58	mpd 15	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
60		risset 3231	. 2 ⊢ ((𝑋 ∧ 𝑌) ∈ 𝐴 ↔ ∃𝑝 ∈ 𝐴 𝑝 = (𝑋 ∧ 𝑌))
61	59, 60	sylibr 235	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081   ≠ wne 2984  ∃wrex 3106   class class class wbr 4966  ‘cfv 6230  (class class class)co 7021  Basecbs 16317  lecple 16406  Posetcpo 17384  meetcmee 17389  0.cp0 17481  Latclat 17489   ⋖ ccvr 35954  Atomscatm 35955  AtLatcal 35956  HLchlt 36042  LLinesclln 36183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-oprab 7025  df-proset 17372  df-poset 17390  df-plt 17402  df-lub 17418  df-glb 17419  df-join 17420  df-meet 17421  df-p0 17483  df-lat 17490  df-clat 17552  df-oposet 35868  df-ol 35870  df-oml 35871  df-covers 35958  df-ats 35959  df-atl 35990  df-cvlat 36014  df-hlat 36043  df-llines 36190

This theorem is referenced by:  2at0mat0  36217  ps-2c  36220  2llnmeqat  36263  dalemcea  36352  dalem2  36353  dalem21  36386  dalem54  36418  cdlemc5  36887