This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme31sn1c

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 1-Mar-2013)

Ref Expression
Hypotheses cdleme31sn1c.g 
|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
cdleme31sn1c.i 
|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
cdleme31sn1c.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme31sn1c.y 
|- Y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( R .\/ t ) ./\ W ) ) )
cdleme31sn1c.c 
|- C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) )
Assertion cdleme31sn1c 
|- ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )

Proof

Step Hyp Ref Expression
1 cdleme31sn1c.g 
 |-  G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
2 cdleme31sn1c.i 
 |-  I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
3 cdleme31sn1c.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , D )
4 cdleme31sn1c.y 
 |-  Y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( R .\/ t ) ./\ W ) ) )
5 cdleme31sn1c.c 
 |-  C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) )
6 eqid 
 |-  ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) )
7 2 3 6 cdleme31sn1 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
8 1 4 cdleme31se 
 |-  ( R e. A -> [_ R / s ]_ G = Y )
9 8 adantr 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ G = Y )
10 9 eqeq2d 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> ( y = [_ R / s ]_ G <-> y = Y ) )
11 10 imbi2d 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> ( ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) <-> ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) ) )
12 11 ralbidv 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) <-> A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) ) )
13 12 riotabidv 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) ) )
14 13 5 eqtr4di 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) = C )
15 7 14 eqtrd 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )