Metamath Proof Explorer

Theorem sprbisymrel

Description: There is a bijection between the subsets of the set of pairs over a fixed set V and the symmetric relations R on the fixed set V . (Contributed by AV, 23-Nov-2021)

Ref Expression
Hypotheses sprsymrelf.p ⊢ P = 𝒫 Pairs ⁡ V
sprsymrelf.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
Assertion sprbisymrel ⊢ V ∈ W → ∃ f f : P ⟶ 1-1 onto R

Proof

Step Hyp Ref Expression
1 sprsymrelf.p ⊢ P = 𝒫 Pairs ⁡ V
2 sprsymrelf.r ⊢ R = r ∈ 𝒫 V × V | ∀ x ∈ V ∀ y ∈ V x r y ↔ y r x
3 fvex ⊢ Pairs ⁡ V ∈ V
4 3 pwex ⊢ 𝒫 Pairs ⁡ V ∈ V
5 1 4 eqeltri ⊢ P ∈ V
6 mptexg ⊢ P ∈ V → p ∈ P ⟼ x y | ∃ c ∈ p c = x y ∈ V
7 5 6 mp1i ⊢ V ∈ W → p ∈ P ⟼ x y | ∃ c ∈ p c = x y ∈ V
8 eqid ⊢ p ∈ P ⟼ x y | ∃ c ∈ p c = x y = p ∈ P ⟼ x y | ∃ c ∈ p c = x y
9 1 2 8 sprsymrelf1o ⊢ V ∈ W → p ∈ P ⟼ x y | ∃ c ∈ p c = x y : P ⟶ 1-1 onto R
10 f1oeq1 ⊢ f = p ∈ P ⟼ x y | ∃ c ∈ p c = x y → f : P ⟶ 1-1 onto R ↔ p ∈ P ⟼ x y | ∃ c ∈ p c = x y : P ⟶ 1-1 onto R
11 10 spcegv ⊢ p ∈ P ⟼ x y | ∃ c ∈ p c = x y ∈ V → p ∈ P ⟼ x y | ∃ c ∈ p c = x y : P ⟶ 1-1 onto R → ∃ f f : P ⟶ 1-1 onto R
12 7 9 11 sylc ⊢ V ∈ W → ∃ f f : P ⟶ 1-1 onto R