Step |
Hyp |
Ref |
Expression |
1 |
|
hashxnn0 |
⊢ ( 𝑃 ∈ 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0* ) |
2 |
|
xnn0le2is012 |
⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0* ∧ ( ♯ ‘ 𝑃 ) ≤ 2 ) → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) ) |
3 |
1 2
|
sylan |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) ≤ 2 ) → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) ) |
4 |
3
|
ex |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) ) ) |
5 |
|
hasheq0 |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 0 ↔ 𝑃 = ∅ ) ) |
6 |
|
eqneqall |
⊢ ( 𝑃 = ∅ → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |
7 |
5 6
|
syl6bi |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
8 |
7
|
com12 |
⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃 ∈ 𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
9 |
|
hash1snb |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 1 ↔ ∃ 𝑐 𝑃 = { 𝑐 } ) ) |
10 |
|
vex |
⊢ 𝑐 ∈ V |
11 |
|
preq12 |
⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑐 ) → { 𝑎 , 𝑏 } = { 𝑐 , 𝑐 } ) |
12 |
|
dfsn2 |
⊢ { 𝑐 } = { 𝑐 , 𝑐 } |
13 |
11 12
|
eqtr4di |
⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑐 ) → { 𝑎 , 𝑏 } = { 𝑐 } ) |
14 |
13
|
eqeq2d |
⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑐 ) → ( 𝑃 = { 𝑎 , 𝑏 } ↔ 𝑃 = { 𝑐 } ) ) |
15 |
10 10 14
|
spc2ev |
⊢ ( 𝑃 = { 𝑐 } → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) |
16 |
15
|
exlimiv |
⊢ ( ∃ 𝑐 𝑃 = { 𝑐 } → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) |
17 |
9 16
|
syl6bi |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 1 → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |
18 |
17
|
imp |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) |
19 |
18
|
a1d |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |
20 |
19
|
expcom |
⊢ ( ( ♯ ‘ 𝑃 ) = 1 → ( 𝑃 ∈ 𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
21 |
|
hash2pr |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) |
22 |
21
|
a1d |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |
23 |
22
|
expcom |
⊢ ( ( ♯ ‘ 𝑃 ) = 2 → ( 𝑃 ∈ 𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
24 |
8 20 23
|
3jaoi |
⊢ ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃 ∈ 𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
25 |
24
|
com12 |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
26 |
4 25
|
syld |
⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ( 𝑃 ≠ ∅ → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
27 |
26
|
com23 |
⊢ ( 𝑃 ∈ 𝑉 → ( 𝑃 ≠ ∅ → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) ) |
28 |
27
|
imp |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |
29 |
|
fveq2 |
⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ { 𝑎 , 𝑏 } ) ) |
30 |
|
hashprlei |
⊢ ( { 𝑎 , 𝑏 } ∈ Fin ∧ ( ♯ ‘ { 𝑎 , 𝑏 } ) ≤ 2 ) |
31 |
30
|
simpri |
⊢ ( ♯ ‘ { 𝑎 , 𝑏 } ) ≤ 2 |
32 |
29 31
|
eqbrtrdi |
⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) ≤ 2 ) |
33 |
32
|
exlimivv |
⊢ ( ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) ≤ 2 ) |
34 |
28 33
|
impbid1 |
⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) |