cnvsym - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnvsym		Structured version Visualization version GIF version

Theorem cnvsym 6019

Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

**Assertion**
Ref	Expression
cnvsym	⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Distinct variable group: 𝑥,𝑦,𝑅

**Proof of Theorem cnvsym**
Step	Hyp	Ref	Expression
1		alcom 2156	. 2 ⊢ (∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
2		relcnv 6012	. . 3 ⊢ Rel ^◡𝑅
3		ssrel 5693	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
4	2, 3	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
5		vex 3436	. . . . . 6 ⊢ 𝑦 ∈ V
6		vex 3436	. . . . . 6 ⊢ 𝑥 ∈ V
7	5, 6	brcnv 5791	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
8		df-br 5075	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
9	7, 8	bitr3i 276	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
10		df-br 5075	. . . 4 ⊢ (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
11	9, 10	imbi12i 351	. . 3 ⊢ ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ (⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
12	11	2albii 1823	. 2 ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
13	1, 4, 12	3bitr4i 303	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 ∈ wcel 2106 ⊆ wss 3887 ⟨cop 4567 class class class wbr 5074 ^◡ccnv 5588 Rel wrel 5594

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-rel 5596 df-cnv 5597

This theorem is referenced by: dfer2 8499 relcnveq3 36456 relcnveq 36457 relcnveq2 36458 cnvcosseq 36560 symrelcoss2 36584 elrelscnveq3 36609 elrelscnveq 36610 elrelscnveq2 36611 dfsymrels3 36660 dfsymrel3 36664 symrefref3 36678 refsymrels3 36680 elrefsymrels3 36684 dfeqvrels3 36702

W3C validator