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 )