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=\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in A\right)\wedge \left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xSy\right)\right)\right)\right\}$$
	fnwe.2	$$⊢\phi \to F:A⟶B$$
	fnwe.3	$$⊢\phi \to R\mathrm{We}B$$
	fnwe.4	$$⊢\phi \to S\mathrm{We}A$$
	fnwe.5	$$⊢\phi \to F\left[w\right]\in \mathrm{V}$$
Assertion	fnwe	$$⊢\phi \to T\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		fnwe.1	$$⊢T=\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in A\right)\wedge \left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xSy\right)\right)\right)\right\}$$
2		fnwe.2	$$⊢\phi \to F:A⟶B$$
3		fnwe.3	$$⊢\phi \to R\mathrm{We}B$$
4		fnwe.4	$$⊢\phi \to S\mathrm{We}A$$
5		fnwe.5	$$⊢\phi \to F\left[w\right]\in \mathrm{V}$$
6		eqid	$$⊢\left\{⟨u,v⟩|\left(\left(u\in \left(B\times A\right)\wedge v\in \left(B\times A\right)\right)\wedge \left(1^{st}\left(u\right)R{1}^{st}\left(v\right)\vee \left(1^{st}\left(u\right)=1^{st}\left(v\right)\wedge 2^{nd}\left(u\right)S{2}^{nd}\left(v\right)\right)\right)\right)\right\}=\left\{⟨u,v⟩|\left(\left(u\in \left(B\times A\right)\wedge v\in \left(B\times A\right)\right)\wedge \left(1^{st}\left(u\right)R{1}^{st}\left(v\right)\vee \left(1^{st}\left(u\right)=1^{st}\left(v\right)\wedge 2^{nd}\left(u\right)S{2}^{nd}\left(v\right)\right)\right)\right)\right\}$$
7		eqid	$$⊢\left(z\in A⟼⟨F\left(z\right),z⟩\right)=\left(z\in A⟼⟨F\left(z\right),z⟩\right)$$
8	1 2 3 4 5 6 7	fnwelem	$$⊢\phi \to T\mathrm{We}A$$