Theorem 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	⊢ Ⅎ 𝑥 𝜓
	cnvoprabOLD.y	⊢ Ⅎ 𝑦 𝜓
	cnvoprabOLD.1	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
	cnvoprabOLD.2	⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
Assertion	cnvoprabOLD	⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cnvoprabOLD.x	⊢ Ⅎ 𝑥 𝜓
2		cnvoprabOLD.y	⊢ Ⅎ 𝑦 𝜓
3		cnvoprabOLD.1	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
4		cnvoprabOLD.2	⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
5		excom	⊢ ( ∃ 𝑎 ∃ 𝑧 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) ↔ ∃ 𝑧 ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
6		nfv	⊢ Ⅎ 𝑥 𝑤 = ⟨ 𝑎 , 𝑧 ⟩
7	6 1	nfan	⊢ Ⅎ 𝑥 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 )
8	7	nfex	⊢ Ⅎ 𝑥 ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 )
9		nfv	⊢ Ⅎ 𝑦 𝑤 = ⟨ 𝑎 , 𝑧 ⟩
10	9 2	nfan	⊢ Ⅎ 𝑦 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 )
11	10	nfex	⊢ Ⅎ 𝑦 ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 )
12		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
13		opeq1	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑎 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
14	13	eqeq2d	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ↔ 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
15	14 3	anbi12d	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) ↔ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
16	12 15	spcev	⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
17	11 16	exlimi	⊢ ( ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
18	8 17	exlimi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
19	4	adantl	⊢ ( ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) → 𝑎 ∈ ( V × V ) )
20		fvex	⊢ ( 1st ‘ 𝑎 ) ∈ V
21		fvex	⊢ ( 2nd ‘ 𝑎 ) ∈ V
22		eqcom	⊢ ( ( 1st ‘ 𝑎 ) = 𝑥 ↔ 𝑥 = ( 1st ‘ 𝑎 ) )
23		eqcom	⊢ ( ( 2nd ‘ 𝑎 ) = 𝑦 ↔ 𝑦 = ( 2nd ‘ 𝑎 ) )
24	22 23	anbi12i	⊢ ( ( ( 1st ‘ 𝑎 ) = 𝑥 ∧ ( 2nd ‘ 𝑎 ) = 𝑦 ) ↔ ( 𝑥 = ( 1st ‘ 𝑎 ) ∧ 𝑦 = ( 2nd ‘ 𝑎 ) ) )
25		eqopi	⊢ ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑎 ) = 𝑥 ∧ ( 2nd ‘ 𝑎 ) = 𝑦 ) ) → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
26	24 25	sylan2br	⊢ ( ( 𝑎 ∈ ( V × V ) ∧ ( 𝑥 = ( 1st ‘ 𝑎 ) ∧ 𝑦 = ( 2nd ‘ 𝑎 ) ) ) → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
27	15	bicomd	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) ) )
28	26 27	syl	⊢ ( ( 𝑎 ∈ ( V × V ) ∧ ( 𝑥 = ( 1st ‘ 𝑎 ) ∧ 𝑦 = ( 2nd ‘ 𝑎 ) ) ) → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) ) )
29	7 10 28	spc2ed	⊢ ( ( 𝑎 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑎 ) ∈ V ∧ ( 2nd ‘ 𝑎 ) ∈ V ) ) → ( ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
30	20 21 29	mpanr12	⊢ ( 𝑎 ∈ ( V × V ) → ( ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
31	19 30	mpcom	⊢ ( ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
32	31	exlimiv	⊢ ( ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
33	18 32	impbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
34	33	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑎 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
35		exrot3	⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
36	5 34 35	3bitr2ri	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑧 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) )
37	36	abbii	⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } = { 𝑤 ∣ ∃ 𝑎 ∃ 𝑧 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) }
38		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
39		df-opab	⊢ { ⟨ 𝑎 , 𝑧 ⟩ ∣ 𝜓 } = { 𝑤 ∣ ∃ 𝑎 ∃ 𝑧 ( 𝑤 = ⟨ 𝑎 , 𝑧 ⟩ ∧ 𝜓 ) }
40	37 38 39	3eqtr4ri	⊢ { ⟨ 𝑎 , 𝑧 ⟩ ∣ 𝜓 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
41	40	cnveqi	⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ 𝜓 } = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
42		cnvopab	⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ 𝜓 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }
43	41 42	eqtr3i	⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }