Theorem dalem20

Description: Lemma for dath . Show that a second dummy atom d exists outside of the Y and Z planes (when those planes are equal). (Contributed by NM, 14-Aug-2012)

	Ref	Expression
Hypotheses	dalem.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
	dalem.l	⊢ ≤ = ( le ‘ 𝐾 )
	dalem.j	⊢ ∨ = ( join ‘ 𝐾 )
	dalem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dalem.ps	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
	dalem20.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
	dalem20.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
	dalem20.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
Assertion	dalem20	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ∃ 𝑐 ∃ 𝑑 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		dalem.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) ∧ ( 𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ) ∧ ( ( ¬ 𝐶 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝐶 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝐶 ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ¬ 𝐶 ≤ ( 𝑆 ∨ 𝑇 ) ∧ ¬ 𝐶 ≤ ( 𝑇 ∨ 𝑈 ) ∧ ¬ 𝐶 ≤ ( 𝑈 ∨ 𝑆 ) ) ∧ ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝑇 ) ∧ 𝐶 ≤ ( 𝑅 ∨ 𝑈 ) ) ) ) )
2		dalem.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dalem.j	⊢ ∨ = ( join ‘ 𝐾 )
4		dalem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dalem.ps	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
6		dalem20.o	⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
7		dalem20.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 )
8		dalem20.z	⊢ 𝑍 = ( ( 𝑆 ∨ 𝑇 ) ∨ 𝑈 )
9	1 2 3 4 7	dalem18	⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝐴 ¬ 𝑐 ≤ 𝑌 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ∃ 𝑐 ∈ 𝐴 ¬ 𝑐 ≤ 𝑌 )
11	1 2 3 4 6 7 8	dalem19	⊢ ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑐 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ) → ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) )
12	11	ex	⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑐 ∈ 𝐴 ) → ( ¬ 𝑐 ≤ 𝑌 → ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
13	12	ancld	⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑐 ∈ 𝐴 ) → ( ¬ 𝑐 ≤ 𝑌 → ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
14	13	reximdva	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( ∃ 𝑐 ∈ 𝐴 ¬ 𝑐 ≤ 𝑌 → ∃ 𝑐 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
15	10 14	mpd	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ∃ 𝑐 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
16		3anass	⊢ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
17	5 16	bitri	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
18	17	2exbii	⊢ ( ∃ 𝑐 ∃ 𝑑 𝜓 ↔ ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
19		r2ex	⊢ ( ∃ 𝑐 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ) )
20		r19.42v	⊢ ( ∃ 𝑑 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ↔ ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
21	20	rexbii	⊢ ( ∃ 𝑐 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ↔ ∃ 𝑐 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
22	18 19 21	3bitr2ri	⊢ ( ∃ 𝑐 ∈ 𝐴 ( ¬ 𝑐 ≤ 𝑌 ∧ ∃ 𝑑 ∈ 𝐴 ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) ↔ ∃ 𝑐 ∃ 𝑑 𝜓 )
23	15 22	sylib	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ∃ 𝑐 ∃ 𝑑 𝜓 )