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

Metamath Proof Explorer

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 )