Theorem cdleme31sdnN

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 31-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme31sdn.c	|- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
	cdleme31sdn.d	|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
	cdleme31sdn.n	|- N = if ( s .<_ ( P .\/ Q ) , I , C )
Assertion	cdleme31sdnN	|- N = if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D )

Proof

Step	Hyp	Ref	Expression
1		cdleme31sdn.c	|- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
2		cdleme31sdn.d	|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
3		cdleme31sdn.n	|- N = if ( s .<_ ( P .\/ Q ) , I , C )
4		biid	|- ( s .<_ ( P .\/ Q ) <-> s .<_ ( P .\/ Q ) )
5	2 1	cdleme31sc	|- ( s e. _V -> [_ s / t ]_ D = C )
6	5	elv	|- [_ s / t ]_ D = C
7	4 6	ifbieq2i	|- if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D ) = if ( s .<_ ( P .\/ Q ) , I , C )
8	3 7	eqtr4i	|- N = if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D )