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

Metamath Proof Explorer

Theorem hash2prb

Description: A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion hash2prb ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )

Proof

Step Hyp Ref Expression
1 hash2exprb ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
2 vex ⊢ 𝑎 ∈ V
3 2 prid1 ⊢ 𝑎 ∈ { 𝑎 , 𝑏 }
4 vex ⊢ 𝑏 ∈ V
5 4 prid2 ⊢ 𝑏 ∈ { 𝑎 , 𝑏 }
6 3 5 pm3.2i ⊢ ( 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } )
7 eleq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ 𝑉 ↔ 𝑎 ∈ { 𝑎 , 𝑏 } ) )
8 eleq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑏 ∈ 𝑉 ↔ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
9 7 8 anbi12d ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ ( 𝑎 ∈ { 𝑎 , 𝑏 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 } ) ) )
10 6 9 mpbiri ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
11 10 adantl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
12 11 pm4.71ri ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
13 12 2exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
14 13 a1i ⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ) )
15 r2ex ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
16 15 bicomi ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )
17 16 a1i ⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
18 1 14 17 3bitrd ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )