This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝑝 ∈ 𝒫 { 𝐴 , 𝐵 } ∣ 𝑝 ≈ 2o } = { { 𝐴 , 𝐵 } } )

Proof

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