Metamath Proof Explorer

Theorem 4atexlemex2

Description: Lemma for 4atexlem7 . Show that when C =/= S , C satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
4thatlem0.l ⊢ ≤ = ( le ‘ 𝐾 )
4thatlem0.j ⊢ ∨ = ( join ‘ 𝐾 )
4thatlem0.m ⊢ ∧ = ( meet ‘ 𝐾 )
4thatlem0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4thatlem0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4thatlem0.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
4thatlem0.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
4thatlem0.c ⊢ 𝐶 = ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) )
Assertion 4atexlemex2 ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 4thatlem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
2 4thatlem0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 4thatlem0.j ⊢ ∨ = ( join ‘ 𝐾 )
4 4thatlem0.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 4thatlem0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 4thatlem0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 4thatlem0.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8 4thatlem0.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
9 4thatlem0.c ⊢ 𝐶 = ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) )
10 1 2 3 4 5 6 7 8 9 4atexlemc ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → 𝐶 ∈ 𝐴 )
12 1 2 3 4 5 6 7 8 9 4atexlemnclw ⊢ ( 𝜑 → ¬ 𝐶 ≤ 𝑊 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → ¬ 𝐶 ≤ 𝑊 )
14 1 2 3 4 5 6 7 8 4atexlemntlpq ⊢ ( 𝜑 → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
15 id ⊢ ( 𝐶 = 𝑃 → 𝐶 = 𝑃 )
16 9 15 syl5eqr ⊢ ( 𝐶 = 𝑃 → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) = 𝑃 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝐶 = 𝑃 ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) = 𝑃 )
18 1 4atexlemkl ⊢ ( 𝜑 → 𝐾 ∈ Lat )
19 1 3 5 4atexlemqtb ⊢ ( 𝜑 → ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
20 1 3 5 4atexlempsb ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 2 4 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑄 ∨ 𝑇 ) )
23 18 19 20 22 syl3anc ⊢ ( 𝜑 → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑄 ∨ 𝑇 ) )
24 1 4atexlemk ⊢ ( 𝜑 → 𝐾 ∈ HL )
25 1 4atexlemq ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
26 1 4atexlemt ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
27 3 5 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑄 ) )
28 24 25 26 27 syl3anc ⊢ ( 𝜑 → ( 𝑄 ∨ 𝑇 ) = ( 𝑇 ∨ 𝑄 ) )
29 23 28 breqtrd ⊢ ( 𝜑 → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑇 ∨ 𝑄 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝑃 ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑇 ∨ 𝑄 ) )
31 17 30 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝑃 ) → 𝑃 ≤ ( 𝑇 ∨ 𝑄 ) )
32 1 4atexlemkc ⊢ ( 𝜑 → 𝐾 ∈ CvLat )
33 1 4atexlemp ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
34 1 4atexlempnq ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
35 2 3 5 cvlatexch2 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ≤ ( 𝑇 ∨ 𝑄 ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) )
36 32 33 26 25 34 35 syl131anc ⊢ ( 𝜑 → ( 𝑃 ≤ ( 𝑇 ∨ 𝑄 ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝑃 ) → ( 𝑃 ≤ ( 𝑇 ∨ 𝑄 ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) )
38 31 37 mpd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝑃 ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) )
39 38 ex ⊢ ( 𝜑 → ( 𝐶 = 𝑃 → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) )
40 39 necon3bd ⊢ ( 𝜑 → ( ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) → 𝐶 ≠ 𝑃 ) )
41 14 40 mpd ⊢ ( 𝜑 → 𝐶 ≠ 𝑃 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → 𝐶 ≠ 𝑃 )
43 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → 𝐶 ≠ 𝑆 )
44 21 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑃 ∨ 𝑆 ) )
45 18 19 20 44 syl3anc ⊢ ( 𝜑 → ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) ) ≤ ( 𝑃 ∨ 𝑆 ) )
46 9 45 eqbrtrid ⊢ ( 𝜑 → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
48 1 4atexlems ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
49 1 2 3 5 4atexlempns ⊢ ( 𝜑 → 𝑃 ≠ 𝑆 )
50 5 2 3 cvlsupr2 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑆 ) → ( ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ↔ ( 𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
51 32 33 48 10 49 50 syl131anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ↔ ( 𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → ( ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ↔ ( 𝐶 ≠ 𝑃 ∧ 𝐶 ≠ 𝑆 ∧ 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) ) ) )
53 42 43 47 52 mpbir3and ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) )
54 breq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 ≤ 𝑊 ↔ 𝐶 ≤ 𝑊 ) )
55 54 notbid ⊢ ( 𝑧 = 𝐶 → ( ¬ 𝑧 ≤ 𝑊 ↔ ¬ 𝐶 ≤ 𝑊 ) )
56 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑃 ∨ 𝑧 ) = ( 𝑃 ∨ 𝐶 ) )
57 oveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑆 ∨ 𝑧 ) = ( 𝑆 ∨ 𝐶 ) )
58 56 57 eqeq12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ↔ ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ) )
59 55 58 anbi12d ⊢ ( 𝑧 = 𝐶 → ( ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ↔ ( ¬ 𝐶 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ) ) )
60 59 rspcev ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( ¬ 𝐶 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝐶 ) = ( 𝑆 ∨ 𝐶 ) ) ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) )
61 11 13 53 60 syl12anc ⊢ ( ( 𝜑 ∧ 𝐶 ≠ 𝑆 ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) )