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 ⊢ A ∈ V ∧ B ∈ W → A ≠ B ↔ A B = 2

Proof

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