Metamath Proof Explorer


Theorem hash2pwpr

Description: If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018)

Ref Expression
Assertion hash2pwpr ( ( ( ♯ ‘ 𝑃 ) = 2 ∧ 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } ) → 𝑃 = { 𝑋 , 𝑌 } )

Proof

Step Hyp Ref Expression
1 pwpr 𝒫 { 𝑋 , 𝑌 } = ( { ∅ , { 𝑋 } } ∪ { { 𝑌 } , { 𝑋 , 𝑌 } } )
2 1 eleq2i ( 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } ↔ 𝑃 ∈ ( { ∅ , { 𝑋 } } ∪ { { 𝑌 } , { 𝑋 , 𝑌 } } ) )
3 elun ( 𝑃 ∈ ( { ∅ , { 𝑋 } } ∪ { { 𝑌 } , { 𝑋 , 𝑌 } } ) ↔ ( 𝑃 ∈ { ∅ , { 𝑋 } } ∨ 𝑃 ∈ { { 𝑌 } , { 𝑋 , 𝑌 } } ) )
4 2 3 bitri ( 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } ↔ ( 𝑃 ∈ { ∅ , { 𝑋 } } ∨ 𝑃 ∈ { { 𝑌 } , { 𝑋 , 𝑌 } } ) )
5 fveq2 ( 𝑃 = ∅ → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ∅ ) )
6 hash0 ( ♯ ‘ ∅ ) = 0
7 6 eqeq2i ( ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ∅ ) ↔ ( ♯ ‘ 𝑃 ) = 0 )
8 eqeq1 ( ( ♯ ‘ 𝑃 ) = 0 → ( ( ♯ ‘ 𝑃 ) = 2 ↔ 0 = 2 ) )
9 0ne2 0 ≠ 2
10 eqneqall ( 0 = 2 → ( 0 ≠ 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
11 9 10 mpi ( 0 = 2 → 𝑃 = { 𝑋 , 𝑌 } )
12 8 11 syl6bi ( ( ♯ ‘ 𝑃 ) = 0 → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
13 7 12 sylbi ( ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ∅ ) → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
14 5 13 syl ( 𝑃 = ∅ → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
15 hashsng ( 𝑋 ∈ V → ( ♯ ‘ { 𝑋 } ) = 1 )
16 fveq2 ( { 𝑋 } = 𝑃 → ( ♯ ‘ { 𝑋 } ) = ( ♯ ‘ 𝑃 ) )
17 16 eqcoms ( 𝑃 = { 𝑋 } → ( ♯ ‘ { 𝑋 } ) = ( ♯ ‘ 𝑃 ) )
18 17 eqeq1d ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ { 𝑋 } ) = 1 ↔ ( ♯ ‘ 𝑃 ) = 1 ) )
19 eqeq1 ( ( ♯ ‘ 𝑃 ) = 1 → ( ( ♯ ‘ 𝑃 ) = 2 ↔ 1 = 2 ) )
20 1ne2 1 ≠ 2
21 eqneqall ( 1 = 2 → ( 1 ≠ 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
22 20 21 mpi ( 1 = 2 → 𝑃 = { 𝑋 , 𝑌 } )
23 19 22 syl6bi ( ( ♯ ‘ 𝑃 ) = 1 → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
24 18 23 syl6bi ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ { 𝑋 } ) = 1 → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
25 15 24 syl5com ( 𝑋 ∈ V → ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
26 snprc ( ¬ 𝑋 ∈ V ↔ { 𝑋 } = ∅ )
27 eqeq2 ( { 𝑋 } = ∅ → ( 𝑃 = { 𝑋 } ↔ 𝑃 = ∅ ) )
28 5 6 eqtrdi ( 𝑃 = ∅ → ( ♯ ‘ 𝑃 ) = 0 )
29 28 eqeq1d ( 𝑃 = ∅ → ( ( ♯ ‘ 𝑃 ) = 2 ↔ 0 = 2 ) )
30 29 11 syl6bi ( 𝑃 = ∅ → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
31 27 30 syl6bi ( { 𝑋 } = ∅ → ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
32 26 31 sylbi ( ¬ 𝑋 ∈ V → ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
33 25 32 pm2.61i ( 𝑃 = { 𝑋 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
34 14 33 jaoi ( ( 𝑃 = ∅ ∨ 𝑃 = { 𝑋 } ) → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
35 hashsng ( 𝑌 ∈ V → ( ♯ ‘ { 𝑌 } ) = 1 )
36 fveq2 ( { 𝑌 } = 𝑃 → ( ♯ ‘ { 𝑌 } ) = ( ♯ ‘ 𝑃 ) )
37 36 eqcoms ( 𝑃 = { 𝑌 } → ( ♯ ‘ { 𝑌 } ) = ( ♯ ‘ 𝑃 ) )
38 37 eqeq1d ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ { 𝑌 } ) = 1 ↔ ( ♯ ‘ 𝑃 ) = 1 ) )
39 38 23 syl6bi ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ { 𝑌 } ) = 1 → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
40 35 39 syl5com ( 𝑌 ∈ V → ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
41 snprc ( ¬ 𝑌 ∈ V ↔ { 𝑌 } = ∅ )
42 eqeq2 ( { 𝑌 } = ∅ → ( 𝑃 = { 𝑌 } ↔ 𝑃 = ∅ ) )
43 5 eqeq1d ( 𝑃 = ∅ → ( ( ♯ ‘ 𝑃 ) = 2 ↔ ( ♯ ‘ ∅ ) = 2 ) )
44 6 eqeq1i ( ( ♯ ‘ ∅ ) = 2 ↔ 0 = 2 )
45 44 11 sylbi ( ( ♯ ‘ ∅ ) = 2 → 𝑃 = { 𝑋 , 𝑌 } )
46 43 45 syl6bi ( 𝑃 = ∅ → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
47 42 46 syl6bi ( { 𝑌 } = ∅ → ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
48 41 47 sylbi ( ¬ 𝑌 ∈ V → ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) ) )
49 40 48 pm2.61i ( 𝑃 = { 𝑌 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
50 ax-1 ( 𝑃 = { 𝑋 , 𝑌 } → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
51 49 50 jaoi ( ( 𝑃 = { 𝑌 } ∨ 𝑃 = { 𝑋 , 𝑌 } ) → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
52 34 51 jaoi ( ( ( 𝑃 = ∅ ∨ 𝑃 = { 𝑋 } ) ∨ ( 𝑃 = { 𝑌 } ∨ 𝑃 = { 𝑋 , 𝑌 } ) ) → ( ( ♯ ‘ 𝑃 ) = 2 → 𝑃 = { 𝑋 , 𝑌 } ) )
53 elpri ( 𝑃 ∈ { ∅ , { 𝑋 } } → ( 𝑃 = ∅ ∨ 𝑃 = { 𝑋 } ) )
54 elpri ( 𝑃 ∈ { { 𝑌 } , { 𝑋 , 𝑌 } } → ( 𝑃 = { 𝑌 } ∨ 𝑃 = { 𝑋 , 𝑌 } ) )
55 53 54 orim12i ( ( 𝑃 ∈ { ∅ , { 𝑋 } } ∨ 𝑃 ∈ { { 𝑌 } , { 𝑋 , 𝑌 } } ) → ( ( 𝑃 = ∅ ∨ 𝑃 = { 𝑋 } ) ∨ ( 𝑃 = { 𝑌 } ∨ 𝑃 = { 𝑋 , 𝑌 } ) ) )
56 52 55 syl11 ( ( ♯ ‘ 𝑃 ) = 2 → ( ( 𝑃 ∈ { ∅ , { 𝑋 } } ∨ 𝑃 ∈ { { 𝑌 } , { 𝑋 , 𝑌 } } ) → 𝑃 = { 𝑋 , 𝑌 } ) )
57 4 56 syl5bi ( ( ♯ ‘ 𝑃 ) = 2 → ( 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } → 𝑃 = { 𝑋 , 𝑌 } ) )
58 57 imp ( ( ( ♯ ‘ 𝑃 ) = 2 ∧ 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } ) → 𝑃 = { 𝑋 , 𝑌 } )