Theorem hash2prd

Description: A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

	Ref	Expression
Assertion	hash2prd	⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		hash2prb	⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
2		simpr	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → 𝑃 = { 𝑥 , 𝑦 } )
3		3simpa	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) )
4	3	ad2antlr	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) )
5		eleq2	⊢ ( 𝑃 = { 𝑥 , 𝑦 } → ( 𝑋 ∈ 𝑃 ↔ 𝑋 ∈ { 𝑥 , 𝑦 } ) )
6		eleq2	⊢ ( 𝑃 = { 𝑥 , 𝑦 } → ( 𝑌 ∈ 𝑃 ↔ 𝑌 ∈ { 𝑥 , 𝑦 } ) )
7	5 6	anbi12d	⊢ ( 𝑃 = { 𝑥 , 𝑦 } → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ↔ ( 𝑋 ∈ { 𝑥 , 𝑦 } ∧ 𝑌 ∈ { 𝑥 , 𝑦 } ) ) )
8	7	adantl	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ↔ ( 𝑋 ∈ { 𝑥 , 𝑦 } ∧ 𝑌 ∈ { 𝑥 , 𝑦 } ) ) )
9	4 8	mpbid	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( 𝑋 ∈ { 𝑥 , 𝑦 } ∧ 𝑌 ∈ { 𝑥 , 𝑦 } ) )
10		prel12g	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( { 𝑋 , 𝑌 } = { 𝑥 , 𝑦 } ↔ ( 𝑋 ∈ { 𝑥 , 𝑦 } ∧ 𝑌 ∈ { 𝑥 , 𝑦 } ) ) )
11	10	ad2antlr	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( { 𝑋 , 𝑌 } = { 𝑥 , 𝑦 } ↔ ( 𝑋 ∈ { 𝑥 , 𝑦 } ∧ 𝑌 ∈ { 𝑥 , 𝑦 } ) ) )
12	9 11	mpbird	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → { 𝑋 , 𝑌 } = { 𝑥 , 𝑦 } )
13	2 12	eqtr4d	⊢ ( ( ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ) ∧ 𝑃 = { 𝑥 , 𝑦 } ) → 𝑃 = { 𝑋 , 𝑌 } )
14	13	exp31	⊢ ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑃 = { 𝑥 , 𝑦 } → 𝑃 = { 𝑋 , 𝑌 } ) ) )
15	14	com23	⊢ ( ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑃 = { 𝑥 , 𝑦 } → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) ) )
16	15	expimpd	⊢ ( ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) ) )
17	16	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) )
18	1 17	syl6bi	⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) ) )
19	18	imp	⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) )