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	$⊢ T = \{⟨x, y⟩ \| ((x \in (A \times B) \land y \in (A \times B)) \land (1^{st} (x) R 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y))))\}$
	Assertion	wexp	$⊢ (R We A \land S We B) \to T We (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		wexp.1	$⊢ T = \{⟨x, y⟩ \| ((x \in (A \times B) \land y \in (A \times B)) \land (1^{st} (x) R 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y))))\}$
2		wefr	$⊢ R We A \to R Fr A$
3		wefr	$⊢ S We B \to S Fr B$
4	1	frxp	$⊢ (R Fr A \land S Fr B) \to T Fr (A \times B)$
5	2 3 4	syl2an	$⊢ (R We A \land S We B) \to T Fr (A \times B)$
6		weso	$⊢ R We A \to R Or A$
7		weso	$⊢ S We B \to S Or B$
8	1	soxp	$⊢ (R Or A \land S Or B) \to T Or (A \times B)$
9	6 7 8	syl2an	$⊢ (R We A \land S We B) \to T Or (A \times B)$
10		df-we	$⊢ T We (A \times B) \leftrightarrow (T Fr (A \times B) \land T Or (A \times B))$
11	5 9 10	sylanbrc	$⊢ (R We A \land S We B) \to T We (A \times B)$