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

Metamath Proof Explorer

Theorem cnvoprab

Description: The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017) (Proof shortened by Thierry Arnoux, 20-Feb-2022)

Ref Expression
Hypotheses cnvoprab.1 ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
cnvoprab.2 ⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
Assertion cnvoprab ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 cnvoprab.1 ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
2 cnvoprab.2 ⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
3 1 dfoprab3 ⊢ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
4 3 cnveqi ⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
5 cnvopab ⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) }
6 inopab ⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) }
7 2 ssopab2i ⊢ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) }
8 sseqin2 ⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ↔ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } )
9 7 8 mpbi ⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }
10 5 6 9 3eqtr2i ⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }
11 4 10 eqtr3i ⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }