This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wexp

Description: A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

		Ref	Expression
	Hypothesis	wexp.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) }
	Assertion	wexp	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑆 We 𝐵 ) → 𝑇 We ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		wexp.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) }
2		wefr	⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
3		wefr	⊢ ( 𝑆 We 𝐵 → 𝑆 Fr 𝐵 )
4	1	frxp	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → 𝑇 Fr ( 𝐴 × 𝐵 ) )
5	2 3 4	syl2an	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑆 We 𝐵 ) → 𝑇 Fr ( 𝐴 × 𝐵 ) )
6		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
7		weso	⊢ ( 𝑆 We 𝐵 → 𝑆 Or 𝐵 )
8	1	soxp	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐴 × 𝐵 ) )
9	6 7 8	syl2an	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑆 We 𝐵 ) → 𝑇 Or ( 𝐴 × 𝐵 ) )
10		df-we	⊢ ( 𝑇 We ( 𝐴 × 𝐵 ) ↔ ( 𝑇 Fr ( 𝐴 × 𝐵 ) ∧ 𝑇 Or ( 𝐴 × 𝐵 ) ) )
11	5 9 10	sylanbrc	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑆 We 𝐵 ) → 𝑇 We ( 𝐴 × 𝐵 ) )