Theorem 2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnj.l	⊢ ≤ = ( le ‘ 𝐾 )
	2llnj.j	⊢ ∨ = ( join ‘ 𝐾 )
	2llnj.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
	2llnj.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion	2llnjN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		2llnj.l	⊢ ≤ = ( le ‘ 𝐾 )
2		2llnj.j	⊢ ∨ = ( join ‘ 𝐾 )
3		2llnj.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
4		2llnj.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	5 2 6 3	islln2	⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ) )
8		simpr	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) )
9	7 8	biimtrdi	⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) )
10	5 2 6 3	islln2	⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) )
11		simpr	⊢ ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) )
12	10 11	biimtrdi	⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
13	9 12	anim12d	⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) )
14	13	imp	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
15	14	3adantr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
16	15	3adant3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) )
17		simp2rr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑋 = ( 𝑞 ∨ 𝑟 ) )
18		simp3rr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑌 = ( 𝑠 ∨ 𝑡 ) )
19	17 18	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) )
20		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
21		breq1	⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≤ 𝑊 ↔ ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ) )
22		neeq1	⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) )
23	21 22	3anbi13d	⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ) )
24		breq1	⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( 𝑌 ≤ 𝑊 ↔ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ) )
25		neeq2	⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) )
26	24 25	3anbi23d	⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
27	23 26	sylan9bb	⊢ ( ( 𝑋 = ( 𝑞 ∨ 𝑟 ) ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
28	17 18 27	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) )
29	20 28	mpbid	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) )
30		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝐾 ∈ HL )
31		simp123	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑊 ∈ 𝑃 )
32		simp2ll	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
33		simp2lr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
34		simp2rl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ≠ 𝑟 )
35		simp3ll	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
36		simp3lr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) )
37		simp3rl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ≠ 𝑡 )
38	1 2 6 3 4	2llnjaN	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) ∧ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 )
39	38	ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) )
40	30 31 32 33 34 35 36 37 39	syl233anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) )
41	29 40	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 )
42	19 41	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )
43	42	3exp	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
44	43	3impib	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
45	44	expd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
46	45	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
47	46	3exp	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) )
48	47	rexlimdvv	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) )
49	48	impd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) )
50	16 49	mpd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 )