qfto

Description: A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013)

		Ref	Expression
	Assertion	qfto	$⊢ A \times B \subseteq R \cup R^{-1} \leftrightarrow \forall x \in A \forall y \in B (x R y \lor y R x)$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
2		brun	$⊢ x (R \cup R^{-1}) y \leftrightarrow (x R y \lor x R^{-1} y)$
3		df-br	$⊢ x (R \cup R^{-1}) y \leftrightarrow ⟨x, y⟩ \in (R \cup R^{-1})$
4		vex	$⊢ x \in V$
5		vex	$⊢ y \in V$
6	4 5	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
7	6	orbi2i	$⊢ (x R y \lor x R^{-1} y) \leftrightarrow (x R y \lor y R x)$
8	2 3 7	3bitr3i	$⊢ ⟨x, y⟩ \in (R \cup R^{-1}) \leftrightarrow (x R y \lor y R x)$
9	1 8	imbi12i	$⊢ (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R \cup R^{-1})) \leftrightarrow ((x \in A \land y \in B) \to (x R y \lor y R x))$
10	9	2albii	$⊢ \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R \cup R^{-1})) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (x R y \lor y R x))$
11		relxp	$⊢ Rel (A \times B)$
12		ssrel	$⊢ Rel (A \times B) \to (A \times B \subseteq R \cup R^{-1} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R \cup R^{-1})))$
13	11 12	ax-mp	$⊢ A \times B \subseteq R \cup R^{-1} \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R \cup R^{-1}))$
14		r2al	$⊢ \forall x \in A \forall y \in B (x R y \lor y R x) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to (x R y \lor y R x))$
15	10 13 14	3bitr4i	$⊢ A \times B \subseteq R \cup R^{-1} \leftrightarrow \forall x \in A \forall y \in B (x R y \lor y R x)$

Metamath Proof Explorer