Theorem dalem19 36852

Description: Lemma for dath 36906. Show that a second dummy atom 𝑑 exists outside of the 𝑌 and 𝑍 planes (when those planes are equal). (Contributed by NM, 15-Aug-2012.)

Hypotheses

Ref	Expression
dalema.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
dalemc.l	⊢ ≤ = (le‘𝐾)
dalemc.j	⊢ ∨ = (join‘𝐾)
dalemc.a	⊢ 𝐴 = (Atoms‘𝐾)
dalem19.o	⊢ 𝑂 = (LPlanes‘𝐾)
dalem19.y	⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
dalem19.z	⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)

Assertion

Ref	Expression
dalem19	⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → ∃𝑑 ∈ 𝐴 (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))

Distinct variable groups:   𝑐,𝑑   𝐴,𝑑   𝐶,𝑑   𝐾,𝑑   ≤ ,𝑑   𝑌,𝑑

Allowed substitution hints:   𝜑(𝑐,𝑑)   𝐴(𝑐)   𝐶(𝑐)   𝑃(𝑐,𝑑)   𝑄(𝑐,𝑑)   𝑅(𝑐,𝑑)   𝑆(𝑐,𝑑)   𝑇(𝑐,𝑑)   𝑈(𝑐,𝑑)   ∨ (𝑐,𝑑)   𝐾(𝑐)   ≤ (𝑐)   𝑂(𝑐,𝑑)   𝑌(𝑐)   𝑍(𝑐,𝑑)

Proof of Theorem dalem19

Step	Hyp	Ref	Expression
1		dalema.ph	. . . 4 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2	1	dalemkehl 36793	. . 3 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	ad3antrrr 728	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → 𝐾 ∈ HL)
4		dalemc.l	. . . 4 ⊢ ≤ = (le‘𝐾)
5		dalemc.j	. . . 4 ⊢ ∨ = (join‘𝐾)
6		dalemc.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
7		dalem19.o	. . . 4 ⊢ 𝑂 = (LPlanes‘𝐾)
8		dalem19.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
9	1, 4, 5, 6, 7, 8	dalemcea 36830	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
10	9	ad3antrrr 728	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → 𝐶 ∈ 𝐴)
11		simplr 767	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → 𝑐 ∈ 𝐴)
12	1, 7	dalemyeb 36819	. . 3 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
13	12	ad3antrrr 728	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → 𝑌 ∈ (Base‘𝐾))
14		dalem19.z	. . . 4 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
15	1, 4, 5, 6, 7, 8, 14	dalem17 36850	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐶 ≤ 𝑌)
16	15	ad2antrr 724	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → 𝐶 ≤ 𝑌)
17		simpr 487	. 2 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → ¬ 𝑐 ≤ 𝑌)
18		eqid 2820	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
19	18, 4, 5, 6	atbtwnex 36618	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ≤ 𝑌 ∧ ¬ 𝑐 ≤ 𝑌)) → ∃𝑑 ∈ 𝐴 (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))
20	3, 10, 11, 13, 16, 17, 19	syl33anc 1380	1 ⊢ ((((𝜑 ∧ 𝑌 = 𝑍) ∧ 𝑐 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌) → ∃𝑑 ∈ 𝐴 (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1082   = wceq 1536   ∈ wcel 2113   ≠ wne 3015  ∃wrex 3138   class class class wbr 5059  ‘cfv 6348  (class class class)co 7149  Basecbs 16476  lecple 16565  joincjn 17547  Atomscatm 36433  HLchlt 36520  LPlanesclpl 36662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-reu 3144  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-proset 17531  df-poset 17549  df-plt 17561  df-lub 17577  df-glb 17578  df-join 17579  df-meet 17580  df-p0 17642  df-lat 17649  df-clat 17711  df-oposet 36346  df-ol 36348  df-oml 36349  df-covers 36436  df-ats 36437  df-atl 36468  df-cvlat 36492  df-hlat 36521  df-llines 36668  df-lplanes 36669

This theorem is referenced by:  dalem20  36863