Theorem hashle2prv

Description: A nonempty subset of a powerset of a class V has size less than or equal to two iff it is an unordered pair of elements of V . (Contributed by AV, 24-Nov-2021)

	Ref	Expression
Assertion	hashle2prv	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ 𝑃 ≠ ∅ ) )
2		hashle2pr	⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ 𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
3	1 2	sylbi	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
4		eldifi	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → 𝑃 ∈ 𝒫 𝑉 )
5		eleq1	⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑃 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
6		prelpw	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
7	6	biimprd	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
8	7	el2v	⊢ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
9	5 8	syl6bi	⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑃 ∈ 𝒫 𝑉 → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
10	4 9	syl5com	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
11	10	pm4.71rd	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝑃 = { 𝑎 , 𝑏 } ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
12	11	2exbidv	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
13		r2ex	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑃 = { 𝑎 , 𝑏 } ) )
14	13	bicomi	⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )
15	14	a1i	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } ) )
16	3 12 15	3bitrd	⊢ ( 𝑃 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } ) )