Metamath Proof Explorer

Theorem elprchashprn2

Description: If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017)

Ref Expression
Assertion elprchashprn2 ( ¬ 𝑀 ∈ V → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )

Proof

Step Hyp Ref Expression
1 prprc1 ⊢ ( ¬ 𝑀 ∈ V → { 𝑀 , 𝑁 } = { 𝑁 } )
2 hashsng ⊢ ( 𝑁 ∈ V → ( ♯ ‘ { 𝑁 } ) = 1 )
3 fveq2 ⊢ ( { 𝑀 , 𝑁 } = { 𝑁 } → ( ♯ ‘ { 𝑀 , 𝑁 } ) = ( ♯ ‘ { 𝑁 } ) )
4 3 eqcomd ⊢ ( { 𝑀 , 𝑁 } = { 𝑁 } → ( ♯ ‘ { 𝑁 } ) = ( ♯ ‘ { 𝑀 , 𝑁 } ) )
5 4 eqeq1d ⊢ ( { 𝑀 , 𝑁 } = { 𝑁 } → ( ( ♯ ‘ { 𝑁 } ) = 1 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 ) )
6 5 biimpa ⊢ ( ( { 𝑀 , 𝑁 } = { 𝑁 } ∧ ( ♯ ‘ { 𝑁 } ) = 1 ) → ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 )
7 id ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 → ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 )
8 1ne2 ⊢ 1 ≠ 2
9 8 a1i ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 → 1 ≠ 2 )
10 7 9 eqnetrd ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 → ( ♯ ‘ { 𝑀 , 𝑁 } ) ≠ 2 )
11 10 neneqd ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 1 → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
12 6 11 syl ⊢ ( ( { 𝑀 , 𝑁 } = { 𝑁 } ∧ ( ♯ ‘ { 𝑁 } ) = 1 ) → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
13 12 expcom ⊢ ( ( ♯ ‘ { 𝑁 } ) = 1 → ( { 𝑀 , 𝑁 } = { 𝑁 } → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
14 2 13 syl ⊢ ( 𝑁 ∈ V → ( { 𝑀 , 𝑁 } = { 𝑁 } → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
15 snprc ⊢ ( ¬ 𝑁 ∈ V ↔ { 𝑁 } = ∅ )
16 eqeq2 ⊢ ( { 𝑁 } = ∅ → ( { 𝑀 , 𝑁 } = { 𝑁 } ↔ { 𝑀 , 𝑁 } = ∅ ) )
17 16 biimpa ⊢ ( ( { 𝑁 } = ∅ ∧ { 𝑀 , 𝑁 } = { 𝑁 } ) → { 𝑀 , 𝑁 } = ∅ )
18 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
19 fveq2 ⊢ ( { 𝑀 , 𝑁 } = ∅ → ( ♯ ‘ { 𝑀 , 𝑁 } ) = ( ♯ ‘ ∅ ) )
20 19 eqcomd ⊢ ( { 𝑀 , 𝑁 } = ∅ → ( ♯ ‘ ∅ ) = ( ♯ ‘ { 𝑀 , 𝑁 } ) )
21 20 eqeq1d ⊢ ( { 𝑀 , 𝑁 } = ∅ → ( ( ♯ ‘ ∅ ) = 0 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 ) )
22 21 biimpa ⊢ ( ( { 𝑀 , 𝑁 } = ∅ ∧ ( ♯ ‘ ∅ ) = 0 ) → ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 )
23 id ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 → ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 )
24 0ne2 ⊢ 0 ≠ 2
25 24 a1i ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 → 0 ≠ 2 )
26 23 25 eqnetrd ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 → ( ♯ ‘ { 𝑀 , 𝑁 } ) ≠ 2 )
27 26 neneqd ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 0 → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
28 22 27 syl ⊢ ( ( { 𝑀 , 𝑁 } = ∅ ∧ ( ♯ ‘ ∅ ) = 0 ) → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
29 17 18 28 sylancl ⊢ ( ( { 𝑁 } = ∅ ∧ { 𝑀 , 𝑁 } = { 𝑁 } ) → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
30 29 ex ⊢ ( { 𝑁 } = ∅ → ( { 𝑀 , 𝑁 } = { 𝑁 } → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
31 15 30 sylbi ⊢ ( ¬ 𝑁 ∈ V → ( { 𝑀 , 𝑁 } = { 𝑁 } → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
32 14 31 pm2.61i ⊢ ( { 𝑀 , 𝑁 } = { 𝑁 } → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )
33 1 32 syl ⊢ ( ¬ 𝑀 ∈ V → ¬ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 )