Metamath Proof Explorer

Theorem cdlemc4

Description: Part of proof of Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses cdlemc3.l ⊢ ≤ ˙ = ≤ K
cdlemc3.j ⊢ ∨ ˙ = join ⁡ K
cdlemc3.m ⊢ ∧ ˙ = meet ⁡ K
cdlemc3.a ⊢ A = Atoms ⁡ K
cdlemc3.h ⊢ H = LHyp ⁡ K
cdlemc3.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemc3.r ⊢ R = trL ⁡ K ⁡ W
Assertion cdlemc4 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ ¬ Q ≤ ˙ P ∨ ˙ F ⁡ P → Q ∨ ˙ R ⁡ F ≠ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W

Proof

Step Hyp Ref Expression
1 cdlemc3.l ⊢ ≤ ˙ = ≤ K
2 cdlemc3.j ⊢ ∨ ˙ = join ⁡ K
3 cdlemc3.m ⊢ ∧ ˙ = meet ⁡ K
4 cdlemc3.a ⊢ A = Atoms ⁡ K
5 cdlemc3.h ⊢ H = LHyp ⁡ K
6 cdlemc3.t ⊢ T = LTrn ⁡ K ⁡ W
7 cdlemc3.r ⊢ R = trL ⁡ K ⁡ W
8 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL
9 8 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ Lat
10 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL ∧ W ∈ H
11 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ∈ T
12 simpr2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∈ A
13 eqid ⊢ Base K = Base K
14 13 4 atbase ⊢ P ∈ A → P ∈ Base K
15 12 14 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∈ Base K
16 13 5 6 ltrncl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ Base K → F ⁡ P ∈ Base K
17 10 11 15 16 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ∈ Base K
18 simpr3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ A
19 13 2 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
20 8 12 18 19 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∨ ˙ Q ∈ Base K
21 13 5 lhpbase ⊢ W ∈ H → W ∈ Base K
22 21 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → W ∈ Base K
23 13 3 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → P ∨ ˙ Q ∧ ˙ W ∈ Base K
24 9 20 22 23 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∨ ˙ Q ∧ ˙ W ∈ Base K
25 13 1 2 latlej1 ⊢ K ∈ Lat ∧ F ⁡ P ∈ Base K ∧ P ∨ ˙ Q ∧ ˙ W ∈ Base K → F ⁡ P ≤ ˙ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
26 9 17 24 25 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ≤ ˙ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
27 breq2 ⊢ Q ∨ ˙ R ⁡ F = F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F ↔ F ⁡ P ≤ ˙ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
28 26 27 syl5ibrcom ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ R ⁡ F = F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F
29 1 2 3 4 5 6 7 cdlemc3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P ≤ ˙ Q ∨ ˙ R ⁡ F → Q ≤ ˙ P ∨ ˙ F ⁡ P
30 28 29 syld ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ R ⁡ F = F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W → Q ≤ ˙ P ∨ ˙ F ⁡ P
31 30 necon3bd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → ¬ Q ≤ ˙ P ∨ ˙ F ⁡ P → Q ∨ ˙ R ⁡ F ≠ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
32 31 3impia ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ ¬ Q ≤ ˙ P ∨ ˙ F ⁡ P → Q ∨ ˙ R ⁡ F ≠ F ⁡ P ∨ ˙ P ∨ ˙ Q ∧ ˙ W