Metamath Proof Explorer

Theorem sprsymrelfv

Description: The value of the function F which maps a subset of the set of pairs over a fixed set V to the relation relating two elements of the set V iff they are in a pair of the subset. (Contributed by AV, 19-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
sprsymrelf.f ⊢ F = p ∈ P ⟼ x y | ∃ c ∈ p c = x y
Assertion sprsymrelfv ⊢ X ∈ P → F ⁡ X = x y | ∃ c ∈ X c = x y

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 sprsymrelf.f ⊢ F = p ∈ P ⟼ x y | ∃ c ∈ p c = x y
4 rexeq ⊢ p = X → ∃ c ∈ p c = x y ↔ ∃ c ∈ X c = x y
5 4 opabbidv ⊢ p = X → x y | ∃ c ∈ p c = x y = x y | ∃ c ∈ X c = x y
6 id ⊢ X ∈ P → X ∈ P
7 elpwi ⊢ X ∈ 𝒫 Pairs ⁡ V → X ⊆ Pairs ⁡ V
8 7 1 eleq2s ⊢ X ∈ P → X ⊆ Pairs ⁡ V
9 sprsymrelfvlem ⊢ X ⊆ Pairs ⁡ V → x y | ∃ c ∈ X c = x y ∈ 𝒫 V × V
10 8 9 syl ⊢ X ∈ P → x y | ∃ c ∈ X c = x y ∈ 𝒫 V × V
11 3 5 6 10 fvmptd3 ⊢ X ∈ P → F ⁡ X = x y | ∃ c ∈ X c = x y