Metamath Proof Explorer

Theorem cdleme50ex

Description: Part of Lemma E in Crawley p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013)

Ref Expression
Hypotheses cdleme.l 
|- .<_ = ( le ` K )
cdleme.a 
|- A = ( Atoms ` K )
cdleme.h 
|- H = ( LHyp ` K )
cdleme.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion cdleme50ex 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E. f e. T ( f ` P ) = Q )

Proof

Step Hyp Ref Expression
1 cdleme.l 
 |-  .<_ = ( le ` K )
2 cdleme.a 
 |-  A = ( Atoms ` K )
3 cdleme.h 
 |-  H = ( LHyp ` K )
4 cdleme.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( meet ` K ) = ( meet ` K )
8 eqid 
 |-  ( ( P ( join ` K ) Q ) ( meet ` K ) W ) = ( ( P ( join ` K ) Q ) ( meet ` K ) W )
9 eqid 
 |-  ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) )
10 eqid 
 |-  ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) )
11 eqid 
 |-  ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) = ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) )
12 5 1 6 7 2 3 8 9 10 11 4 cdleme50ltrn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) e. T )
13 5 1 6 7 2 3 8 9 10 11 cdleme17d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) ` P ) = Q )
14 fveq1 
 |-  ( f = ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) -> ( f ` P ) = ( ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) ` P ) )
15 14 eqeq1d 
 |-  ( f = ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) -> ( ( f ` P ) = Q <-> ( ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) ` P ) = Q ) )
16 15 rspcev 
 |-  ( ( ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) e. T /\ ( ( x e. ( Base ` K ) |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. ( Base ` K ) A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. ( Base ` K ) A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) ` P ) = Q ) -> E. f e. T ( f ` P ) = Q )
17 12 13 16 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> E. f e. T ( f ` P ) = Q )