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 ∧ 𝑃 ∈ 𝒫 { 𝑋 , 𝑌 } ) → 𝑃 = { 𝑋 , 𝑌 } )