Metamath Proof Explorer

Theorem cdlemkuv2-2

Description: Part of proof of Lemma K of Crawley p. 118. Line 16 on p. 119 for i = 2, where sigma_2 (p) is V , f_2 is C , and k_2 is Q . (Contributed by NM, 2-Jul-2013)

Ref Expression
Hypotheses cdlemk2.b ⊢ B = Base K
cdlemk2.l ⊢ ≤ ˙ = ≤ K
cdlemk2.j ⊢ ∨ ˙ = join ⁡ K
cdlemk2.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk2.a ⊢ A = Atoms ⁡ K
cdlemk2.h ⊢ H = LHyp ⁡ K
cdlemk2.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk2.r ⊢ R = trL ⁡ K ⁡ W
cdlemk2.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
cdlemk2.q ⊢ Q = S ⁡ C
cdlemk2.v ⊢ V = d ∈ T ⟼ ι k ∈ T | k ⁡ P = P ∨ ˙ R ⁡ d ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ d ∘ C -1
Assertion cdlemkuv2-2 ⊢ K ∈ HL ∧ W ∈ H ∧ R ⁡ F = R ⁡ N ∧ G ∈ T ∧ F ∈ T ∧ C ∈ T ∧ N ∈ T ∧ R ⁡ C ≠ R ⁡ F ∧ R ⁡ C ≠ R ⁡ G ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ C ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → V ⁡ G ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ G ∘ C -1

Proof

Step Hyp Ref Expression
1 cdlemk2.b ⊢ B = Base K
2 cdlemk2.l ⊢ ≤ ˙ = ≤ K
3 cdlemk2.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk2.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemk2.a ⊢ A = Atoms ⁡ K
6 cdlemk2.h ⊢ H = LHyp ⁡ K
7 cdlemk2.t ⊢ T = LTrn ⁡ K ⁡ W
8 cdlemk2.r ⊢ R = trL ⁡ K ⁡ W
9 cdlemk2.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
10 cdlemk2.q ⊢ Q = S ⁡ C
11 cdlemk2.v ⊢ V = d ∈ T ⟼ ι k ∈ T | k ⁡ P = P ∨ ˙ R ⁡ d ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ d ∘ C -1
12 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 ⊢ K ∈ HL ∧ W ∈ H ∧ R ⁡ F = R ⁡ N ∧ G ∈ T ∧ F ∈ T ∧ C ∈ T ∧ N ∈ T ∧ R ⁡ C ≠ R ⁡ F ∧ R ⁡ C ≠ R ⁡ G ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ C ≠ I ↾ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → V ⁡ G ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ Q ⁡ P ∨ ˙ R ⁡ G ∘ C -1