cnvoprabOLD

Description: The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab as of 16-Oct-2022, which has nonfreeness hypotheses instead of disjoint variable conditions. (Contributed by Thierry Arnoux, 17-Aug-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnvoprabOLD.x	$⊢ Ⅎ x ψ$
	cnvoprabOLD.y	$⊢ Ⅎ y ψ$
	cnvoprabOLD.1	$⊢ a = ⟨x, y⟩ \to (ψ \leftrightarrow φ)$
	cnvoprabOLD.2	$⊢ ψ \to a \in (V \times V)$
Assertion	cnvoprabOLD	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1} = \{⟨z, a⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		cnvoprabOLD.x	$⊢ Ⅎ x ψ$
2		cnvoprabOLD.y	$⊢ Ⅎ y ψ$
3		cnvoprabOLD.1	$⊢ a = ⟨x, y⟩ \to (ψ \leftrightarrow φ)$
4		cnvoprabOLD.2	$⊢ ψ \to a \in (V \times V)$
5		excom	$⊢ \exists a \exists z (w = ⟨a, z⟩ \land ψ) \leftrightarrow \exists z \exists a (w = ⟨a, z⟩ \land ψ)$
6		nfv	$⊢ Ⅎ x w = ⟨a, z⟩$
7	6 1	nfan	$⊢ Ⅎ x (w = ⟨a, z⟩ \land ψ)$
8	7	nfex	$⊢ Ⅎ x \exists a (w = ⟨a, z⟩ \land ψ)$
9		nfv	$⊢ Ⅎ y w = ⟨a, z⟩$
10	9 2	nfan	$⊢ Ⅎ y (w = ⟨a, z⟩ \land ψ)$
11	10	nfex	$⊢ Ⅎ y \exists a (w = ⟨a, z⟩ \land ψ)$
12		opex	$⊢ ⟨x, y⟩ \in V$
13		opeq1	$⊢ a = ⟨x, y⟩ \to ⟨a, z⟩ = ⟨⟨x, y⟩, z⟩$
14	13	eqeq2d	$⊢ a = ⟨x, y⟩ \to (w = ⟨a, z⟩ \leftrightarrow w = ⟨⟨x, y⟩, z⟩)$
15	14 3	anbi12d	$⊢ a = ⟨x, y⟩ \to ((w = ⟨a, z⟩ \land ψ) \leftrightarrow (w = ⟨⟨x, y⟩, z⟩ \land φ))$
16	12 15	spcev	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists a (w = ⟨a, z⟩ \land ψ)$
17	11 16	exlimi	$⊢ \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists a (w = ⟨a, z⟩ \land ψ)$
18	8 17	exlimi	$⊢ \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists a (w = ⟨a, z⟩ \land ψ)$
19	4	adantl	$⊢ (w = ⟨a, z⟩ \land ψ) \to a \in (V \times V)$
20		fvex	$⊢ 1^{st} (a) \in V$
21		fvex	$⊢ 2^{nd} (a) \in V$
22		eqcom	$⊢ 1^{st} (a) = x \leftrightarrow x = 1^{st} (a)$
23		eqcom	$⊢ 2^{nd} (a) = y \leftrightarrow y = 2^{nd} (a)$
24	22 23	anbi12i	$⊢ (1^{st} (a) = x \land 2^{nd} (a) = y) \leftrightarrow (x = 1^{st} (a) \land y = 2^{nd} (a))$
25		eqopi	$⊢ (a \in (V \times V) \land (1^{st} (a) = x \land 2^{nd} (a) = y)) \to a = ⟨x, y⟩$
26	24 25	sylan2br	$⊢ (a \in (V \times V) \land (x = 1^{st} (a) \land y = 2^{nd} (a))) \to a = ⟨x, y⟩$
27	15	bicomd	$⊢ a = ⟨x, y⟩ \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (w = ⟨a, z⟩ \land ψ))$
28	26 27	syl	$⊢ (a \in (V \times V) \land (x = 1^{st} (a) \land y = 2^{nd} (a))) \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (w = ⟨a, z⟩ \land ψ))$
29	7 10 28	spc2ed	$⊢ (a \in (V \times V) \land (1^{st} (a) \in V \land 2^{nd} (a) \in V)) \to ((w = ⟨a, z⟩ \land ψ) \to \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ))$
30	20 21 29	mpanr12	$⊢ a \in (V \times V) \to ((w = ⟨a, z⟩ \land ψ) \to \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ))$
31	19 30	mpcom	$⊢ (w = ⟨a, z⟩ \land ψ) \to \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ)$
32	31	exlimiv	$⊢ \exists a (w = ⟨a, z⟩ \land ψ) \to \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ)$
33	18 32	impbii	$⊢ \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists a (w = ⟨a, z⟩ \land ψ)$
34	33	exbii	$⊢ \exists z \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists z \exists a (w = ⟨a, z⟩ \land ψ)$
35		exrot3	$⊢ \exists z \exists x \exists y (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
36	5 34 35	3bitr2ri	$⊢ \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists a \exists z (w = ⟨a, z⟩ \land ψ)$
37	36	abbii	$⊢ \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\} = \{w \| \exists a \exists z (w = ⟨a, z⟩ \land ψ)\}$
38		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
39		df-opab	$⊢ \{⟨a, z⟩ \| ψ\} = \{w \| \exists a \exists z (w = ⟨a, z⟩ \land ψ)\}$
40	37 38 39	3eqtr4ri	$⊢ \{⟨a, z⟩ \| ψ\} = \{⟨⟨x, y⟩, z⟩ \| φ\}$
41	40	cnveqi	$⊢ {\{⟨a, z⟩ \| ψ\}}^{-1} = {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1}$
42		cnvopab	$⊢ {\{⟨a, z⟩ \| ψ\}}^{-1} = \{⟨z, a⟩ \| ψ\}$
43	41 42	eqtr3i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\}}^{-1} = \{⟨z, a⟩ \| ψ\}$

Metamath Proof Explorer

Theorem cnvoprabOLD

Proof