This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvsym

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) (Proof shortened by SN, 23-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ◡ 𝑅
2 ssrel3 ⊢ ( Rel ◡ 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ) )
3 1 2 ax-mp ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) )
4 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑧 ◡ 𝑅 𝑥 ) )
5 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
6 4 5 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑧 ◡ 𝑅 𝑥 → 𝑧 𝑅 𝑥 ) ) )
7 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑦 ◡ 𝑅 𝑧 ) )
8 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 ) )
9 7 8 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ◡ 𝑅 𝑧 → 𝑦 𝑅 𝑧 ) ) )
10 6 9 alcomw ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) )
11 vex ⊢ 𝑦 ∈ V
12 vex ⊢ 𝑥 ∈ V
13 11 12 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
14 13 imbi1i ⊢ ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
15 14 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
16 3 10 15 3bitri ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )