Theorem prprspr2

Description: The set of all proper unordered pairs over a given set V is the set of all unordered pairs over that set of size two. (Contributed by AV, 29-Apr-2023)

	Ref	Expression
Assertion	prprspr2	⊢ ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		sprval	⊢ ( 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } } )
2	1	abeq2d	⊢ ( 𝑉 ∈ V → ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ) )
3	2	anbi1d	⊢ ( 𝑉 ∈ V → ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ) )
4		r19.41vv	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
5		fveqeq2	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
6		hashprg	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
7	6	el2v	⊢ ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
8	5 7	bitr4di	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ 𝑎 ≠ 𝑏 ) )
9	8	pm5.32i	⊢ ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ( 𝑝 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
10	9	biancomi	⊢ ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) )
11	10	a1i	⊢ ( ( 𝑉 ∈ V ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
12	11	2rexbidva	⊢ ( 𝑉 ∈ V → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
13	4 12	bitr3id	⊢ ( 𝑉 ∈ V → ( ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑝 = { 𝑎 , 𝑏 } ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
14	3 13	bitrd	⊢ ( 𝑉 ∈ V → ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) )
15	14	abbidv	⊢ ( 𝑉 ∈ V → { 𝑝 ∣ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) } = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )
16		df-rab	⊢ { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } = { 𝑝 ∣ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) }
17	16	a1i	⊢ ( 𝑉 ∈ V → { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } = { 𝑝 ∣ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) } )
18		prprval	⊢ ( 𝑉 ∈ V → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )
19	15 17 18	3eqtr4rd	⊢ ( 𝑉 ∈ V → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
20		rab0	⊢ { 𝑝 ∈ ∅ ∣ ( ♯ ‘ 𝑝 ) = 2 } = ∅
21	20	a1i	⊢ ( ¬ 𝑉 ∈ V → { 𝑝 ∈ ∅ ∣ ( ♯ ‘ 𝑝 ) = 2 } = ∅ )
22		fvprc	⊢ ( ¬ 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = ∅ )
23	22	rabeqdv	⊢ ( ¬ 𝑉 ∈ V → { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } = { 𝑝 ∈ ∅ ∣ ( ♯ ‘ 𝑝 ) = 2 } )
24		fvprc	⊢ ( ¬ 𝑉 ∈ V → ( Pairsproper ‘ 𝑉 ) = ∅ )
25	21 23 24	3eqtr4rd	⊢ ( ¬ 𝑉 ∈ V → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
26	19 25	pm2.61i	⊢ ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 }