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 5695

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 2201	. 2 ⊢ (∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
2		relcnv 5687	. . 3 ⊢ Rel ^◡𝑅
3		ssrel 5379	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
4	2, 3	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
5		vex 3353	. . . . . 6 ⊢ 𝑦 ∈ V
6		vex 3353	. . . . . 6 ⊢ 𝑥 ∈ V
7	5, 6	brcnv 5475	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
8		df-br 4812	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
9	7, 8	bitr3i 268	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
10		df-br 4812	. . . 4 ⊢ (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
11	9, 10	imbi12i 341	. . 3 ⊢ ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ (⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
12	11	2albii 1915	. 2 ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
13	1, 4, 12	3bitr4i 294	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∀wal 1650 ∈ wcel 2155 ⊆ wss 3734 ⟨cop 4342 class class class wbr 4811 ^◡ccnv 5278 Rel wrel 5284

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-sep 4943 ax-nul 4951 ax-pr 5064

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-rab 3064 df-v 3352 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-nul 4082 df-if 4246 df-sn 4337 df-pr 4339 df-op 4343 df-br 4812 df-opab 4874 df-xp 5285 df-rel 5286 df-cnv 5287

This theorem is referenced by: dfer2 7952 relcnveq3 34542 relcnveq 34543 relcnveq2 34544 cnvcosseq 34642 symrelcoss2 34666 elrelscnveq3 34691 elrelscnveq 34692 elrelscnveq2 34693 dfsymrels3 34742 dfsymrel3 34746 symrefref3 34760 refsymrels3 34762 elrefsymrels3 34766 dfeqvrels3 34783

W3C validator