Theorem fnwe

Description: A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013) (Revised by Mario Carneiro, 18-Nov-2014)

	Ref	Expression
Hypotheses	fnwe.1	|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
	fnwe.2	|- ( ph -> F : A --> B )
	fnwe.3	|- ( ph -> R We B )
	fnwe.4	|- ( ph -> S We A )
	fnwe.5	|- ( ph -> ( F " w ) e. _V )
Assertion	fnwe	|- ( ph -> T We A )

Proof

Step	Hyp	Ref	Expression
1		fnwe.1	|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
2		fnwe.2	|- ( ph -> F : A --> B )
3		fnwe.3	|- ( ph -> R We B )
4		fnwe.4	|- ( ph -> S We A )
5		fnwe.5	|- ( ph -> ( F " w ) e. _V )
6		eqid	|- { <. u , v >. | ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) } = { <. u , v >. | ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) }
7		eqid	|- ( z e. A |-> <. ( F ` z ) , z >. ) = ( z e. A |-> <. ( F ` z ) , z >. )
8	1 2 3 4 5 6 7	fnwelem	|- ( ph -> T We A )