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	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
	sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
	sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
Assertion	sprsymrelfv	⊢ ( 𝑋 ∈ 𝑃 → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } } )

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	⊢ 𝑃 = 𝒫 ( Pairs ‘ 𝑉 )
2		sprsymrelf.r	⊢ 𝑅 = { 𝑟 ∈ 𝒫 ( 𝑉 × 𝑉 ) ∣ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 𝑟 𝑦 ↔ 𝑦 𝑟 𝑥 ) }
3		sprsymrelf.f	⊢ 𝐹 = ( 𝑝 ∈ 𝑃 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } )
4		rexeq	⊢ ( 𝑝 = 𝑋 → ( ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } ) )
5	4	opabbidv	⊢ ( 𝑝 = 𝑋 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑝 𝑐 = { 𝑥 , 𝑦 } } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } } )
6		id	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ 𝑃 )
7		elpwi	⊢ ( 𝑋 ∈ 𝒫 ( Pairs ‘ 𝑉 ) → 𝑋 ⊆ ( Pairs ‘ 𝑉 ) )
8	7 1	eleq2s	⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ⊆ ( Pairs ‘ 𝑉 ) )
9		sprsymrelfvlem	⊢ ( 𝑋 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
10	8 9	syl	⊢ ( 𝑋 ∈ 𝑃 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
11	3 5 6 10	fvmptd3	⊢ ( 𝑋 ∈ 𝑃 → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑋 𝑐 = { 𝑥 , 𝑦 } } )