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	$⊢ a = ⟨x, y⟩ \to (ψ \leftrightarrow φ)$
		cnvoprab.2	$⊢ ψ \to a \in (V \times V)$
	Assertion	cnvoprab	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1} = \{⟨z, a⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		cnvoprab.1	$⊢ a = ⟨x, y⟩ \to (ψ \leftrightarrow φ)$
2		cnvoprab.2	$⊢ ψ \to a \in (V \times V)$
3	1	dfoprab3	$⊢ \{⟨a, z⟩ \| (a \in (V \times V) \land ψ)\} = \{⟨⟨x, y⟩, z⟩ \| φ\}$
4	3	cnveqi	$⊢ {\{⟨a, z⟩ \| (a \in (V \times V) \land ψ)\}}^{-1} = {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1}$
5		cnvopab	$⊢ {\{⟨a, z⟩ \| (a \in (V \times V) \land ψ)\}}^{-1} = \{⟨z, a⟩ \| (a \in (V \times V) \land ψ)\}$
6		inopab	$⊢ \{⟨z, a⟩ \| a \in (V \times V)\} \cap \{⟨z, a⟩ \| ψ\} = \{⟨z, a⟩ \| (a \in (V \times V) \land ψ)\}$
7	2	ssopab2i	$⊢ \{⟨z, a⟩ \| ψ\} \subseteq \{⟨z, a⟩ \| a \in (V \times V)\}$
8		sseqin2	$⊢ \{⟨z, a⟩ \| ψ\} \subseteq \{⟨z, a⟩ \| a \in (V \times V)\} \leftrightarrow \{⟨z, a⟩ \| a \in (V \times V)\} \cap \{⟨z, a⟩ \| ψ\} = \{⟨z, a⟩ \| ψ\}$
9	7 8	mpbi	$⊢ \{⟨z, a⟩ \| a \in (V \times V)\} \cap \{⟨z, a⟩ \| ψ\} = \{⟨z, a⟩ \| ψ\}$
10	5 6 9	3eqtr2i	$⊢ {\{⟨a, z⟩ \| (a \in (V \times V) \land ψ)\}}^{-1} = \{⟨z, a⟩ \| ψ\}$
11	4 10	eqtr3i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1} = \{⟨z, a⟩ \| ψ\}$