Metamath Proof Explorer

Theorem cdleme0ex2N

Description: Part of proof of Lemma E in Crawley p. 113. Note that ( P .\/ u ) = ( Q .\/ u ) is a shorter way to express u =/= P /\ u =/= Q /\ u .<_ ( P .\/ Q ) . (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme0.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme0.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme0.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme0.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion cdleme0ex2N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑢 ∈ 𝐴 ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ∧ 𝑢 ≤ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdleme0.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme0.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme0.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme0.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
9 simp2rl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 )
10 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 )
11 1 2 3 4 5 6 cdleme0ex1N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑊 ) )
12 7 8 9 10 11 syl121anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑊 ) )
13 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝐾 ∈ HL )
14 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
15 13 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝐾 ∈ CvLat )
16 simp2ll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 )
17 16 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑃 ∈ 𝐴 )
18 9 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑄 ∈ 𝐴 )
19 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ∈ 𝐴 )
20 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑃 ≠ 𝑄 )
21 4 1 2 cvlsupr2 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ↔ ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
22 15 17 18 19 20 21 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ↔ ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
23 df-3an ⊢ ( ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ ( ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ) ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
24 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ≤ 𝑊 )
25 simp2lr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑃 ≤ 𝑊 )
26 25 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ¬ 𝑃 ≤ 𝑊 )
27 nbrne2 ⊢ ( ( 𝑢 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑢 ≠ 𝑃 )
28 24 26 27 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ≠ 𝑃 )
29 simp2rr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑄 ≤ 𝑊 )
30 29 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ¬ 𝑄 ≤ 𝑊 )
31 nbrne2 ⊢ ( ( 𝑢 ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊 ) → 𝑢 ≠ 𝑄 )
32 24 30 31 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → 𝑢 ≠ 𝑄 )
33 28 32 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ) )
34 33 biantrurd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ) ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
35 23 34 bitr4id ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ( ( 𝑢 ≠ 𝑃 ∧ 𝑢 ≠ 𝑄 ∧ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
36 22 35 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑢 ≤ 𝑊 ) → ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ↔ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) )
37 36 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 ≤ 𝑊 → ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ↔ 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
38 37 pm5.32rd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑢 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ∧ 𝑢 ≤ 𝑊 ) ↔ ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑊 ) ) )
39 38 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ∃ 𝑢 ∈ 𝐴 ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ∧ 𝑢 ≤ 𝑊 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑢 ≤ 𝑊 ) ) )
40 12 39 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑢 ∈ 𝐴 ( ( 𝑃 ∨ 𝑢 ) = ( 𝑄 ∨ 𝑢 ) ∧ 𝑢 ≤ 𝑊 ) )