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 6008

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 2158	. 2 ⊢ (∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
2		relcnv 6001	. . 3 ⊢ Rel ^◡𝑅
3		ssrel 5683	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
4	2, 3	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
5		vex 3426	. . . . . 6 ⊢ 𝑦 ∈ V
6		vex 3426	. . . . . 6 ⊢ 𝑥 ∈ V
7	5, 6	brcnv 5780	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
8		df-br 5071	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
9	7, 8	bitr3i 276	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
10		df-br 5071	. . . 4 ⊢ (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
11	9, 10	imbi12i 350	. . 3 ⊢ ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ (⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
12	11	2albii 1824	. 2 ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
13	1, 4, 12	3bitr4i 302	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 ∈ wcel 2108 ⊆ wss 3883 ⟨cop 4564 class class class wbr 5070 ^◡ccnv 5579 Rel wrel 5585

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-br 5071 df-opab 5133 df-xp 5586 df-rel 5587 df-cnv 5588

This theorem is referenced by: dfer2 8457 relcnveq3 36383 relcnveq 36384 relcnveq2 36385 cnvcosseq 36487 symrelcoss2 36511 elrelscnveq3 36536 elrelscnveq 36537 elrelscnveq2 36538 dfsymrels3 36587 dfsymrel3 36591 symrefref3 36605 refsymrels3 36607 elrefsymrels3 36611 dfeqvrels3 36629

W3C validator