Theorem hashprb

Description: The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018)

	Ref	Expression
Assertion	hashprb	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		hashprg	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( 𝑀 ≠ 𝑁 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
2	1	biimp3a	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) → ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
3		elprchashprn2	⊢ ( ¬ 𝑀 ∈ V → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
4		pm2.21	⊢ ( ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ) )
5	3 4	syl	⊢ ( ¬ 𝑀 ∈ V → ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ) )
6		elprchashprn2	⊢ ( ¬ 𝑁 ∈ V → ¬ ( ♯ ‘ { 𝑁 , 𝑀 } ) = 2 )
7		prcom	⊢ { 𝑁 , 𝑀 } = { 𝑀 , 𝑁 }
8	7	fveq2i	⊢ ( ♯ ‘ { 𝑁 , 𝑀 } ) = ( ♯ ‘ { 𝑀 , 𝑁 } )
9	8	eqeq1i	⊢ ( ( ♯ ‘ { 𝑁 , 𝑀 } ) = 2 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
10	9 4	sylnbi	⊢ ( ¬ ( ♯ ‘ { 𝑁 , 𝑀 } ) = 2 → ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ) )
11	6 10	syl	⊢ ( ¬ 𝑁 ∈ V → ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ) )
12		simpll	⊢ ( ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → 𝑀 ∈ V )
13		simplr	⊢ ( ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → 𝑁 ∈ V )
14	1	biimpar	⊢ ( ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → 𝑀 ≠ 𝑁 )
15	12 13 14	3jca	⊢ ( ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) )
16	15	ex	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ) )
17	5 11 16	ecase	⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) )
18	2 17	impbii	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁 ) ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )