Theorem prprelprb

Description: A set is an element of the set of all proper unordered pairs over a given set X iff it is a pair of different elements of the set X . (Contributed by AV, 7-May-2023)

	Ref	Expression
Assertion	prprelprb	⊢ ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prprvalpw	⊢ ( 𝑋 ∈ V → ( Pairsproper ‘ 𝑋 ) = { 𝑝 ∈ 𝒫 𝑋 ∣ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )
2	1	eleq2d	⊢ ( 𝑋 ∈ V → ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑋 ∣ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ) )
3		eqeq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 = { 𝑎 , 𝑏 } ↔ 𝑃 = { 𝑎 , 𝑏 } ) )
4	3	anbi2d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
5	4	2rexbidv	⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
6	5	elrab	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑋 ∣ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ↔ ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
7	2 6	bitrdi	⊢ ( 𝑋 ∈ V → ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ) )
8		pm3.22	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
9	8	a1i	⊢ ( ( 𝑃 ∈ 𝒫 𝑋 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
10	9	reximdvva	⊢ ( 𝑃 ∈ 𝒫 𝑋 → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
11	10	imp	⊢ ( ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
12	11	anim2i	⊢ ( ( 𝑋 ∈ V ∧ ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ) → ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
13	12	ex	⊢ ( 𝑋 ∈ V → ( ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) → ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
14		simpr	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
15	14	ancomd	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) )
16		prelpwi	⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 )
17	16	adantl	⊢ ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 )
18	17	adantr	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 )
19		eleq1	⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑃 ∈ 𝒫 𝑋 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 ) )
20	19	adantr	⊢ ( ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( 𝑃 ∈ 𝒫 𝑋 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 ) )
21	20	adantl	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑃 ∈ 𝒫 𝑋 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑋 ) )
22	18 21	mpbird	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑃 ∈ 𝒫 𝑋 )
23	15 22	jca	⊢ ( ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) )
24	23	ex	⊢ ( ( 𝑋 ∈ V ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) ) )
25	24	reximdvva	⊢ ( 𝑋 ∈ V → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) ) )
26	25	imp	⊢ ( ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) )
27		r19.41vv	⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) ↔ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) )
28	27	biancomi	⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ∧ 𝑃 ∈ 𝒫 𝑋 ) ↔ ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
29	26 28	sylib	⊢ ( ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
30	13 29	impbid1	⊢ ( 𝑋 ∈ V → ( ( 𝑃 ∈ 𝒫 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
31	7 30	bitrd	⊢ ( 𝑋 ∈ V → ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
32		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( Pairsproper ‘ 𝑋 ) = ∅ )
33	32	eleq2d	⊢ ( ¬ 𝑋 ∈ V → ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ 𝑃 ∈ ∅ ) )
34		noel	⊢ ¬ 𝑃 ∈ ∅
35		pm2.21	⊢ ( ¬ 𝑃 ∈ ∅ → ( 𝑃 ∈ ∅ → ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
36	34 35	mp1i	⊢ ( ¬ 𝑋 ∈ V → ( 𝑃 ∈ ∅ → ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
37		pm2.21	⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 ∈ V → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → 𝑃 ∈ ∅ ) ) )
38	37	impd	⊢ ( ¬ 𝑋 ∈ V → ( ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → 𝑃 ∈ ∅ ) )
39	36 38	impbid	⊢ ( ¬ 𝑋 ∈ V → ( 𝑃 ∈ ∅ ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
40	33 39	bitrd	⊢ ( ¬ 𝑋 ∈ V → ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) ) )
41	31 40	pm2.61i	⊢ ( 𝑃 ∈ ( Pairsproper ‘ 𝑋 ) ↔ ( 𝑋 ∈ V ∧ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑃 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )