Metamath Proof Explorer

Theorem pr2pwpr

Description: The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pr2pwpr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → p ∈ 𝒫 A B | p ≈ 2 𝑜 = A B

Proof

Step Hyp Ref Expression
1 elpwi ⊢ s ∈ 𝒫 A B → s ⊆ A B
2 prfi ⊢ A B ∈ Fin
3 ssfi ⊢ A B ∈ Fin ∧ s ⊆ A B → s ∈ Fin
4 2 3 mpan ⊢ s ⊆ A B → s ∈ Fin
5 hash2 ⊢ 2 𝑜 = 2
6 5 eqcomi ⊢ 2 = 2 𝑜
7 6 a1i ⊢ s ∈ Fin → 2 = 2 𝑜
8 7 eqeq2d ⊢ s ∈ Fin → s = 2 ↔ s = 2 𝑜
9 2onn ⊢ 2 𝑜 ∈ ω
10 nnfi ⊢ 2 𝑜 ∈ ω → 2 𝑜 ∈ Fin
11 9 10 ax-mp ⊢ 2 𝑜 ∈ Fin
12 hashen ⊢ s ∈ Fin ∧ 2 𝑜 ∈ Fin → s = 2 𝑜 ↔ s ≈ 2 𝑜
13 11 12 mpan2 ⊢ s ∈ Fin → s = 2 𝑜 ↔ s ≈ 2 𝑜
14 8 13 bitrd ⊢ s ∈ Fin → s = 2 ↔ s ≈ 2 𝑜
15 hash2pwpr ⊢ s = 2 ∧ s ∈ 𝒫 A B → s = A B
16 15 a1d ⊢ s = 2 ∧ s ∈ 𝒫 A B → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
17 16 ex ⊢ s = 2 → s ∈ 𝒫 A B → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
18 14 17 syl6bir ⊢ s ∈ Fin → s ≈ 2 𝑜 → s ∈ 𝒫 A B → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
19 18 com23 ⊢ s ∈ Fin → s ∈ 𝒫 A B → s ≈ 2 𝑜 → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
20 4 19 syl ⊢ s ⊆ A B → s ∈ 𝒫 A B → s ≈ 2 𝑜 → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
21 1 20 mpcom ⊢ s ∈ 𝒫 A B → s ≈ 2 𝑜 → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
22 21 imp ⊢ s ∈ 𝒫 A B ∧ s ≈ 2 𝑜 → A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B
23 22 com12 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → s ∈ 𝒫 A B ∧ s ≈ 2 𝑜 → s = A B
24 prex ⊢ A B ∈ V
25 24 prid2 ⊢ A B ∈ B A B
26 25 a1i ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ∈ B A B
27 26 olcd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ∈ ∅ A ∨ A B ∈ B A B
28 elun ⊢ A B ∈ ∅ A ∪ B A B ↔ A B ∈ ∅ A ∨ A B ∈ B A B
29 27 28 sylibr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ∈ ∅ A ∪ B A B
30 pwpr ⊢ 𝒫 A B = ∅ A ∪ B A B
31 29 30 eleqtrrdi ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ∈ 𝒫 A B
32 31 adantr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → A B ∈ 𝒫 A B
33 eleq1 ⊢ s = A B → s ∈ 𝒫 A B ↔ A B ∈ 𝒫 A B
34 33 adantl ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → s ∈ 𝒫 A B ↔ A B ∈ 𝒫 A B
35 32 34 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → s ∈ 𝒫 A B
36 pr2nelem ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≈ 2 𝑜
37 36 adantr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → A B ≈ 2 𝑜
38 breq1 ⊢ s = A B → s ≈ 2 𝑜 ↔ A B ≈ 2 𝑜
39 38 adantl ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → s ≈ 2 𝑜 ↔ A B ≈ 2 𝑜
40 37 39 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → s ≈ 2 𝑜
41 35 40 jca ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ s = A B → s ∈ 𝒫 A B ∧ s ≈ 2 𝑜
42 41 ex ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → s = A B → s ∈ 𝒫 A B ∧ s ≈ 2 𝑜
43 23 42 impbid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → s ∈ 𝒫 A B ∧ s ≈ 2 𝑜 ↔ s = A B
44 breq1 ⊢ p = s → p ≈ 2 𝑜 ↔ s ≈ 2 𝑜
45 44 elrab ⊢ s ∈ p ∈ 𝒫 A B | p ≈ 2 𝑜 ↔ s ∈ 𝒫 A B ∧ s ≈ 2 𝑜
46 velsn ⊢ s ∈ A B ↔ s = A B
47 43 45 46 3bitr4g ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → s ∈ p ∈ 𝒫 A B | p ≈ 2 𝑜 ↔ s ∈ A B
48 47 eqrdv ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → p ∈ 𝒫 A B | p ≈ 2 𝑜 = A B