This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opabn1stprc

Description: An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion opabn1stprc ( ∃ 𝑦 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 biantrur ⊢ ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
3 2 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
4 3 dmeqi ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
5 id ⊢ ( ∃ 𝑦 𝜑 → ∃ 𝑦 𝜑 )
6 5 ralrimivw ⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∈ V ∃ 𝑦 𝜑 )
7 dmopab3 ⊢ ( ∀ 𝑥 ∈ V ∃ 𝑦 𝜑 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) } = V )
8 6 7 sylib ⊢ ( ∃ 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) } = V )
9 4 8 eqtrid ⊢ ( ∃ 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = V )
10 vprc ⊢ ¬ V ∈ V
11 10 a1i ⊢ ( ∃ 𝑦 𝜑 → ¬ V ∈ V )
12 9 11 eqneltrd ⊢ ( ∃ 𝑦 𝜑 → ¬ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
13 dmexg ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
14 12 13 nsyl ⊢ ( ∃ 𝑦 𝜑 → ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
15 df-nel ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V ↔ ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
16 14 15 sylibr ⊢ ( ∃ 𝑦 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V )