This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) ) )
19 18 imp ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑃 = { 𝑋 , 𝑌 } ) )