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	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
	fnwe.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fnwe.3	⊢ ( 𝜑 → 𝑅 We 𝐵 )
	fnwe.4	⊢ ( 𝜑 → 𝑆 We 𝐴 )
	fnwe.5	⊢ ( 𝜑 → ( 𝐹 “ 𝑤 ) ∈ V )
Assertion	fnwe	⊢ ( 𝜑 → 𝑇 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnwe.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑆 𝑦 ) ) ) }
2		fnwe.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3		fnwe.3	⊢ ( 𝜑 → 𝑅 We 𝐵 )
4		fnwe.4	⊢ ( 𝜑 → 𝑆 We 𝐴 )
5		fnwe.5	⊢ ( 𝜑 → ( 𝐹 “ 𝑤 ) ∈ V )
6		eqid	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 1^st ‘ 𝑢 ) 𝑅 ( 1^st ‘ 𝑣 ) ∨ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑣 ) ∧ ( 2^nd ‘ 𝑢 ) 𝑆 ( 2^nd ‘ 𝑣 ) ) ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝐵 × 𝐴 ) ∧ 𝑣 ∈ ( 𝐵 × 𝐴 ) ) ∧ ( ( 1^st ‘ 𝑢 ) 𝑅 ( 1^st ‘ 𝑣 ) ∨ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑣 ) ∧ ( 2^nd ‘ 𝑢 ) 𝑆 ( 2^nd ‘ 𝑣 ) ) ) ) }
7		eqid	⊢ ( 𝑧 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ ) = ( 𝑧 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑧 ) , 𝑧 ⟩ )
8	1 2 3 4 5 6 7	fnwelem	⊢ ( 𝜑 → 𝑇 We 𝐴 )

Metamath Proof Explorer

Theorem fnwe

Proof