Metamath Proof Explorer


Theorem cdleme50f

Description: Part of proof of Lemma D in Crawley p. 113. TODO: fix comment. TODO: can we use just F Fn B since range is computed in cdleme50rn ? (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B = Base K
cdlemef50.l ˙ = K
cdlemef50.j ˙ = join K
cdlemef50.m ˙ = meet K
cdlemef50.a A = Atoms K
cdlemef50.h H = LHyp K
cdlemef50.u U = P ˙ Q ˙ W
cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef50.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
Assertion cdleme50f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F : B B

Proof

Step Hyp Ref Expression
1 cdlemef50.b B = Base K
2 cdlemef50.l ˙ = K
3 cdlemef50.j ˙ = join K
4 cdlemef50.m ˙ = meet K
5 cdlemef50.a A = Atoms K
6 cdlemef50.h H = LHyp K
7 cdlemef50.u U = P ˙ Q ˙ W
8 cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef50.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
11 riotaex ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W V
12 vex x V
13 11 12 ifex if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x V
14 13 a1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x V
15 10 a1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
16 vex s V
17 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
18 8 17 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
19 16 18 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
20 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
21 eqid if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D
22 eqid ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W
23 1 2 3 4 5 6 7 19 8 9 20 21 22 10 cdleme32fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W e B F e B
24 14 15 23 fmpt2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F : B B