relcnveq2 - Mathbox for Peter Mazsa

	Mathbox for Peter Mazsa		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > relcnveq2		Structured version Visualization version GIF version

Theorem relcnveq2 35582

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.)

**Assertion**
Ref	Expression
relcnveq2	⊢ (Rel 𝑅 → (^◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))

Distinct variable group: 𝑥,𝑅,𝑦

**Proof of Theorem relcnveq2**
Step	Hyp	Ref	Expression
1		cnvsym 5976	. . . 4 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
2	1	a1i 11	. . 3 ⊢ (Rel 𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
3		cnvsym 5976	. . . . 5 ⊢ (^◡^◡𝑅 ⊆ ^◡𝑅 ↔ ∀𝑥∀𝑦(𝑥^◡𝑅𝑦 → 𝑦^◡𝑅𝑥))
4		dfrel2 6048	. . . . . . 7 ⊢ (Rel 𝑅 ↔ ^◡^◡𝑅 = 𝑅)
5	4	biimpi 218	. . . . . 6 ⊢ (Rel 𝑅 → ^◡^◡𝑅 = 𝑅)
6	5	sseq1d 4000	. . . . 5 ⊢ (Rel 𝑅 → (^◡^◡𝑅 ⊆ ^◡𝑅 ↔ 𝑅 ⊆ ^◡𝑅))
7	3, 6	syl5rbbr 288	. . . 4 ⊢ (Rel 𝑅 → (𝑅 ⊆ ^◡𝑅 ↔ ∀𝑥∀𝑦(𝑥^◡𝑅𝑦 → 𝑦^◡𝑅𝑥)))
8		relbrcnvg 5970	. . . . . 6 ⊢ (Rel 𝑅 → (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥))
9		relbrcnvg 5970	. . . . . 6 ⊢ (Rel 𝑅 → (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦))
10	8, 9	imbi12d 347	. . . . 5 ⊢ (Rel 𝑅 → ((𝑥^◡𝑅𝑦 → 𝑦^◡𝑅𝑥) ↔ (𝑦𝑅𝑥 → 𝑥𝑅𝑦)))
11	10	2albidv 1924	. . . 4 ⊢ (Rel 𝑅 → (∀𝑥∀𝑦(𝑥^◡𝑅𝑦 → 𝑦^◡𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦𝑅𝑥 → 𝑥𝑅𝑦)))
12	7, 11	bitrd 281	. . 3 ⊢ (Rel 𝑅 → (𝑅 ⊆ ^◡𝑅 ↔ ∀𝑥∀𝑦(𝑦𝑅𝑥 → 𝑥𝑅𝑦)))
13	2, 12	anbi12d 632	. 2 ⊢ (Rel 𝑅 → ((^◡𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ^◡𝑅) ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦(𝑦𝑅𝑥 → 𝑥𝑅𝑦))))
14		eqss 3984	. 2 ⊢ (^◡𝑅 = 𝑅 ↔ (^◡𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ^◡𝑅))
15		2albiim 1891	. 2 ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦(𝑦𝑅𝑥 → 𝑥𝑅𝑦)))
16	13, 14, 15	3bitr4g 316	1 ⊢ (Rel 𝑅 → (^◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 = wceq 1537 ⊆ wss 3938 class class class wbr 5068 ^◡ccnv 5556 Rel wrel 5562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-xp 5563 df-rel 5564 df-cnv 5565

This theorem is referenced by: relcnveq4 35583

W3C validator