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 ⊢ P = x ∈ 𝒫 V | x = 2
Assertion prpair ⊢ X ∈ P ↔ ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b

Proof

Step Hyp Ref Expression
1 prpair.p ⊢ P = x ∈ 𝒫 V | x = 2
2 1 eleq2i ⊢ X ∈ P ↔ X ∈ x ∈ 𝒫 V | x = 2
3 fveqeq2 ⊢ x = X → x = 2 ↔ X = 2
4 3 elrab ⊢ X ∈ x ∈ 𝒫 V | x = 2 ↔ X ∈ 𝒫 V ∧ X = 2
5 hash2prb ⊢ X ∈ 𝒫 V → X = 2 ↔ ∃ a ∈ X ∃ b ∈ X a ≠ b ∧ X = a b
6 elpwi ⊢ X ∈ 𝒫 V → X ⊆ V
7 ancom ⊢ a ≠ b ∧ X = a b ↔ X = a b ∧ a ≠ b
8 7 2rexbii ⊢ ∃ a ∈ X ∃ b ∈ X a ≠ b ∧ X = a b ↔ ∃ a ∈ X ∃ b ∈ X X = a b ∧ a ≠ b
9 8 biimpi ⊢ ∃ a ∈ X ∃ b ∈ X a ≠ b ∧ X = a b → ∃ a ∈ X ∃ b ∈ X X = a b ∧ a ≠ b
10 ss2rexv ⊢ X ⊆ V → ∃ a ∈ X ∃ b ∈ X X = a b ∧ a ≠ b → ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
11 6 9 10 syl2im ⊢ X ∈ 𝒫 V → ∃ a ∈ X ∃ b ∈ X a ≠ b ∧ X = a b → ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
12 5 11 sylbid ⊢ X ∈ 𝒫 V → X = 2 → ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
13 12 imp ⊢ X ∈ 𝒫 V ∧ X = 2 → ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
14 prelpwi ⊢ a ∈ V ∧ b ∈ V → a b ∈ 𝒫 V
15 14 adantr ⊢ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → a b ∈ 𝒫 V
16 hashprg ⊢ a ∈ V ∧ b ∈ V → a ≠ b ↔ a b = 2
17 16 biimpd ⊢ a ∈ V ∧ b ∈ V → a ≠ b → a b = 2
18 17 adantld ⊢ a ∈ V ∧ b ∈ V → X = a b ∧ a ≠ b → a b = 2
19 18 imp ⊢ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → a b = 2
20 eleq1 ⊢ X = a b → X ∈ 𝒫 V ↔ a b ∈ 𝒫 V
21 fveqeq2 ⊢ X = a b → X = 2 ↔ a b = 2
22 20 21 anbi12d ⊢ X = a b → X ∈ 𝒫 V ∧ X = 2 ↔ a b ∈ 𝒫 V ∧ a b = 2
23 22 adantr ⊢ X = a b ∧ a ≠ b → X ∈ 𝒫 V ∧ X = 2 ↔ a b ∈ 𝒫 V ∧ a b = 2
24 23 adantl ⊢ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → X ∈ 𝒫 V ∧ X = 2 ↔ a b ∈ 𝒫 V ∧ a b = 2
25 15 19 24 mpbir2and ⊢ a ∈ V ∧ b ∈ V ∧ X = a b ∧ a ≠ b → X ∈ 𝒫 V ∧ X = 2
26 25 ex ⊢ a ∈ V ∧ b ∈ V → X = a b ∧ a ≠ b → X ∈ 𝒫 V ∧ X = 2
27 26 rexlimivv ⊢ ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b → X ∈ 𝒫 V ∧ X = 2
28 13 27 impbii ⊢ X ∈ 𝒫 V ∧ X = 2 ↔ ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b
29 2 4 28 3bitri ⊢ X ∈ P ↔ ∃ a ∈ V ∃ b ∈ V X = a b ∧ a ≠ b