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

Metamath Proof Explorer

Theorem qfto

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

		Ref	Expression
	Assertion	qfto	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑅 ∪ ^◡ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
2		brun	⊢ ( 𝑥 ( 𝑅 ∪ ^◡ 𝑅 ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑥 ^◡ 𝑅 𝑦 ) )
3		df-br	⊢ ( 𝑥 ( 𝑅 ∪ ^◡ 𝑅 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) )
4		vex	⊢ 𝑥 ∈ V
5		vex	⊢ 𝑦 ∈ V
6	4 5	brcnv	⊢ ( 𝑥 ^◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
7	6	orbi2i	⊢ ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 ^◡ 𝑅 𝑦 ) ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
8	2 3 7	3bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
9	1 8	imbi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
10	9	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
11		relxp	⊢ Rel ( 𝐴 × 𝐵 )
12		ssrel	⊢ ( Rel ( 𝐴 × 𝐵 ) → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑅 ∪ ^◡ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) ) ) )
13	11 12	ax-mp	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑅 ∪ ^◡ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ^◡ 𝑅 ) ) )
14		r2al	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
15	10 13 14	3bitr4i	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝑅 ∪ ^◡ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )