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 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )