qfto - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > qfto		GIF version

Theorem qfto 4993

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

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

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐵,𝑦 𝑥,𝑅,𝑦

**Proof of Theorem qfto**
Step	Hyp	Ref	Expression
1		opelxp 4634	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2		brun 4033	. . . . 5 ⊢ (𝑥(𝑅 ∪ ^◡𝑅)𝑦 ↔ (𝑥𝑅𝑦 ∨ 𝑥^◡𝑅𝑦))
3		df-br 3983	. . . . 5 ⊢ (𝑥(𝑅 ∪ ^◡𝑅)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅))
4		vex 2729	. . . . . . 7 ⊢ 𝑥 ∈ V
5		vex 2729	. . . . . . 7 ⊢ 𝑦 ∈ V
6	4, 5	brcnv 4787	. . . . . 6 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
7	6	orbi2i 752	. . . . 5 ⊢ ((𝑥𝑅𝑦 ∨ 𝑥^◡𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))
8	2, 3, 7	3bitr3i 209	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅) ↔ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))
9	1, 8	imbi12i 238	. . 3 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
10	9	2albii 1459	. 2 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
11		relxp 4713	. . 3 ⊢ Rel (𝐴 × 𝐵)
12		ssrel 4692	. . 3 ⊢ (Rel (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ^◡𝑅) ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅))))
13	11, 12	ax-mp 5	. 2 ⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ^◡𝑅) ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑅 ∪ ^◡𝑅)))
14		r2al 2485	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
15	10, 13, 14	3bitr4i 211	1 ⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ^◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 ∀wal 1341 ∈ wcel 2136 ∀wral 2444 ∪ cun 3114 ⊆ wss 3116 ⟨cop 3579 class class class wbr 3982 × cxp 4602 ^◡ccnv 4603 Rel wrel 4609

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-pow 4153 ax-pr 4187

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ral 2449 df-rex 2450 df-v 2728 df-un 3120 df-in 3122 df-ss 3129 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-br 3983 df-opab 4044 df-xp 4610 df-rel 4611 df-cnv 4612

This theorem is referenced by: (None)

W3C validator