Theorem hashle2pr

Description: A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021)

	Ref	Expression
Assertion	hashle2pr	⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) )

Proof

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	biimtrdi	⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 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	biimtrdi	⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 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 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) )