Metamath Proof Explorer

Theorem hashprg

Description: The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013) (Revised by Mario Carneiro, 5-May-2016) (Revised by AV, 18-Sep-2021)

Ref Expression
Assertion hashprg ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
2 elsni ⊢ ( 𝐵 ∈ { 𝐴 } → 𝐵 = 𝐴 )
3 2 eqcomd ⊢ ( 𝐵 ∈ { 𝐴 } → 𝐴 = 𝐵 )
4 3 necon3ai ⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ { 𝐴 } )
5 snfi ⊢ { 𝐴 } ∈ Fin
6 hashunsng ⊢ ( 𝐵 ∈ 𝑊 → ( ( { 𝐴 } ∈ Fin ∧ ¬ 𝐵 ∈ { 𝐴 } ) → ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( ♯ ‘ { 𝐴 } ) + 1 ) ) )
7 6 imp ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ( { 𝐴 } ∈ Fin ∧ ¬ 𝐵 ∈ { 𝐴 } ) ) → ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( ♯ ‘ { 𝐴 } ) + 1 ) )
8 5 7 mpanr1 ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ { 𝐴 } ) → ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( ♯ ‘ { 𝐴 } ) + 1 ) )
9 1 4 8 syl2an ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( ♯ ‘ { 𝐴 } ) + 1 ) )
10 hashsng ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝐴 } ) = 1 )
11 10 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ♯ ‘ { 𝐴 } ) = 1 )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 } ) = 1 )
13 12 oveq1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ♯ ‘ { 𝐴 } ) + 1 ) = ( 1 + 1 ) )
14 9 13 eqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( 1 + 1 ) )
15 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
16 15 fveq2i ⊢ ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ ( { 𝐴 } ∪ { 𝐵 } ) )
17 df-2 ⊢ 2 = ( 1 + 1 )
18 14 16 17 3eqtr4g ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
19 1ne2 ⊢ 1 ≠ 2
20 19 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 1 ≠ 2 )
21 11 20 eqnetrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ♯ ‘ { 𝐴 } ) ≠ 2 )
22 dfsn2 ⊢ { 𝐴 } = { 𝐴 , 𝐴 }
23 preq2 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
24 22 23 eqtr2id ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
25 24 fveq2d ⊢ ( 𝐴 = 𝐵 → ( ♯ ‘ { 𝐴 , 𝐵 } ) = ( ♯ ‘ { 𝐴 } ) )
26 25 neeq1d ⊢ ( 𝐴 = 𝐵 → ( ( ♯ ‘ { 𝐴 , 𝐵 } ) ≠ 2 ↔ ( ♯ ‘ { 𝐴 } ) ≠ 2 ) )
27 21 26 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → ( ♯ ‘ { 𝐴 , 𝐵 } ) ≠ 2 ) )
28 27 necon2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 → 𝐴 ≠ 𝐵 ) )
29 28 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) → 𝐴 ≠ 𝐵 )
30 18 29 impbida ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )