Metamath Proof Explorer

Theorem prpair

Description: Characterization of a proper pair: A class is a proper pair iff it consists of exactly two different sets. (Contributed by AV, 11-Mar-2023)

Ref Expression
Hypothesis prpair.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion prpair ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )

Proof

Step Hyp Ref Expression
1 prpair.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 1 eleq2i ⊢ ( 𝑋 ∈ 𝑃 ↔ 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
3 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ 𝑋 ) = 2 ) )
4 3 elrab ⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) )
5 hash2prb ⊢ ( 𝑋 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑋 ) = 2 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑎 , 𝑏 } ) ) )
6 elpwi ⊢ ( 𝑋 ∈ 𝒫 𝑉 → 𝑋 ⊆ 𝑉 )
7 ancom ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑎 , 𝑏 } ) ↔ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
8 7 2rexbii ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
9 8 biimpi ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
10 ss2rexv ⊢ ( 𝑋 ⊆ 𝑉 → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
11 6 9 10 syl2im ⊢ ( 𝑋 ∈ 𝒫 𝑉 → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
12 5 11 sylbid ⊢ ( 𝑋 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑋 ) = 2 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
13 12 imp ⊢ ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
14 prelpwi ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 )
15 14 adantr ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 )
16 hashprg ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
17 16 biimpd ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ≠ 𝑏 → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
18 17 adantld ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
19 18 imp ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
20 eleq1 ⊢ ( 𝑋 = { 𝑎 , 𝑏 } → ( 𝑋 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
21 fveqeq2 ⊢ ( 𝑋 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑋 ) = 2 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
22 20 21 anbi12d ⊢ ( 𝑋 = { 𝑎 , 𝑏 } → ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) ) )
23 22 adantr ⊢ ( ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) ) )
24 23 adantl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) ) )
25 15 19 24 mpbir2and ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) )
26 25 ex ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) ) )
27 26 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) → ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) )
28 13 27 impbii ⊢ ( ( 𝑋 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑋 ) = 2 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
29 2 4 28 3bitri ⊢ ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑋 = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )