Theorem cdlemefr29exN

Description: Lemma for cdlemefs29bpre1N . (Compare cdleme25a .) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemefr29.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemefr29.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemefr29.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemefr29.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemefr29.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemefr29.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	cdlemefr29exN	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ∃ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemefr29.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemefr29.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemefr29.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemefr29.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdlemefr29.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdlemefr29.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
9	1 2 3 4 5 6	lhpmcvr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
10	7 8 9	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
11		nfv	⊢ Ⅎ 𝑠 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
12		nfv	⊢ Ⅎ 𝑠 ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
13		nfra1	⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵
14	11 12 13	nf3an	⊢ Ⅎ 𝑠 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 )
15		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → 𝐾 ∈ HL )
16	15	adantr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
17	16	hllatd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
18		simpl3	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 )
19		simprl	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → 𝑠 ∈ 𝐴 )
20		rsp	⊢ ( ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 → ( 𝑠 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
21	18 19 20	sylc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → 𝐶 ∈ 𝐵 )
22	15	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → 𝐾 ∈ Lat )
23		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
24		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → 𝑊 ∈ 𝐻 )
25	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
26	24 25	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → 𝑊 ∈ 𝐵 )
27	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
28	22 23 26 27	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
29	28	adantr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
30	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
31	17 21 29 30	syl3anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
32	31	expr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑠 ≤ 𝑊 → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) )
33	32	adantrd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) )
34	33	ancld	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) ) )
35	34	ex	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( 𝑠 ∈ 𝐴 → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) ) ) )
36	14 35	reximdai	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ∃ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) ) )
37	10 36	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ ∀ 𝑠 ∈ 𝐴 𝐶 ∈ 𝐵 ) → ∃ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 ) )