Theorem prelspr

Description: An unordered pair of elements of a fixed set V belongs to the set of all unordered pairs over the set V . (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	prelspr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		prelpwi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 )
2		eqidd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } = { 𝑋 , 𝑌 } )
3		preq1	⊢ ( 𝑎 = 𝑋 → { 𝑎 , 𝑏 } = { 𝑋 , 𝑏 } )
4	3	eqeq2d	⊢ ( 𝑎 = 𝑋 → ( { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ↔ { 𝑋 , 𝑌 } = { 𝑋 , 𝑏 } ) )
5		preq2	⊢ ( 𝑏 = 𝑌 → { 𝑋 , 𝑏 } = { 𝑋 , 𝑌 } )
6	5	eqeq2d	⊢ ( 𝑏 = 𝑌 → ( { 𝑋 , 𝑌 } = { 𝑋 , 𝑏 } ↔ { 𝑋 , 𝑌 } = { 𝑋 , 𝑌 } ) )
7	4 6	rspc2ev	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } = { 𝑋 , 𝑌 } ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } )
8	2 7	mpd3an3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } )
9	1 8	jca	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ) )
10	9	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ) )
11		eqeq1	⊢ ( 𝑝 = { 𝑋 , 𝑌 } → ( 𝑝 = { 𝑎 , 𝑏 } ↔ { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ) )
12	11	2rexbidv	⊢ ( 𝑝 = { 𝑋 , 𝑌 } → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ) )
13	12	elrab	⊢ ( { 𝑋 , 𝑌 } ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } ↔ ( { 𝑋 , 𝑌 } ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ) )
14	10 13	sylibr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → { 𝑋 , 𝑌 } ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
15		sprvalpw	⊢ ( 𝑉 ∈ 𝑊 → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
16	15	adantr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( Pairs ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
17	14 16	eleqtrrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) )