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∈𝒫AB|p≈2𝑜=AB

Proof

Step Hyp Ref Expression
1 elpwi ⊢s∈𝒫AB→s⊆AB
2 prfi ⊢AB∈Fin
3 ssfi ⊢AB∈Fin∧s⊆AB→s∈Fin
4 2 3 mpan ⊢s⊆AB→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∈𝒫AB→s=AB
16 15 a1d ⊢s=2∧s∈𝒫AB→A∈V∧B∈W∧A≠B→s=AB
17 16 ex ⊢s=2→s∈𝒫AB→A∈V∧B∈W∧A≠B→s=AB
18 14 17 syl6bir ⊢s∈Fin→s≈2𝑜→s∈𝒫AB→A∈V∧B∈W∧A≠B→s=AB
19 18 com23 ⊢s∈Fin→s∈𝒫AB→s≈2𝑜→A∈V∧B∈W∧A≠B→s=AB
20 4 19 syl ⊢s⊆AB→s∈𝒫AB→s≈2𝑜→A∈V∧B∈W∧A≠B→s=AB
21 1 20 mpcom ⊢s∈𝒫AB→s≈2𝑜→A∈V∧B∈W∧A≠B→s=AB
22 21 imp ⊢s∈𝒫AB∧s≈2𝑜→A∈V∧B∈W∧A≠B→s=AB
23 22 com12 ⊢A∈V∧B∈W∧A≠B→s∈𝒫AB∧s≈2𝑜→s=AB
24 prex ⊢AB∈V
25 24 prid2 ⊢AB∈BAB
26 25 a1i ⊢A∈V∧B∈W∧A≠B→AB∈BAB
27 26 olcd ⊢A∈V∧B∈W∧A≠B→AB∈∅A∨AB∈BAB
28 elun ⊢AB∈∅A∪BAB↔AB∈∅A∨AB∈BAB
29 27 28 sylibr ⊢A∈V∧B∈W∧A≠B→AB∈∅A∪BAB
30 pwpr ⊢𝒫AB=∅A∪BAB
31 29 30 eleqtrrdi ⊢A∈V∧B∈W∧A≠B→AB∈𝒫AB
32 31 adantr ⊢A∈V∧B∈W∧A≠B∧s=AB→AB∈𝒫AB
33 eleq1 ⊢s=AB→s∈𝒫AB↔AB∈𝒫AB
34 33 adantl ⊢A∈V∧B∈W∧A≠B∧s=AB→s∈𝒫AB↔AB∈𝒫AB
35 32 34 mpbird ⊢A∈V∧B∈W∧A≠B∧s=AB→s∈𝒫AB
36 enpr2 ⊢A∈V∧B∈W∧A≠B→AB≈2𝑜
37 36 adantr ⊢A∈V∧B∈W∧A≠B∧s=AB→AB≈2𝑜
38 breq1 ⊢s=AB→s≈2𝑜↔AB≈2𝑜
39 38 adantl ⊢A∈V∧B∈W∧A≠B∧s=AB→s≈2𝑜↔AB≈2𝑜
40 37 39 mpbird ⊢A∈V∧B∈W∧A≠B∧s=AB→s≈2𝑜
41 35 40 jca ⊢A∈V∧B∈W∧A≠B∧s=AB→s∈𝒫AB∧s≈2𝑜
42 41 ex ⊢A∈V∧B∈W∧A≠B→s=AB→s∈𝒫AB∧s≈2𝑜
43 23 42 impbid ⊢A∈V∧B∈W∧A≠B→s∈𝒫AB∧s≈2𝑜↔s=AB
44 breq1 ⊢p=s→p≈2𝑜↔s≈2𝑜
45 44 elrab ⊢s∈p∈𝒫AB|p≈2𝑜↔s∈𝒫AB∧s≈2𝑜
46 velsn ⊢s∈AB↔s=AB
47 43 45 46 3bitr4g ⊢A∈V∧B∈W∧A≠B→s∈p∈𝒫AB|p≈2𝑜↔s∈AB
48 47 eqrdv ⊢A∈V∧B∈W∧A≠B→p∈𝒫AB|p≈2𝑜=AB