Theorem eloi 10659

Description: A consequence of membership in a class abstraction whose elements belong to ((V X. V) X. (V X. V)) using ordered pair extractors.

Hypotheses

Ref	Expression
eloi.1	|- (y = (1st` (1st` A)) -> (ph <-> ps))
eloi.2	|- (z = (2nd` (1st` A)) -> (ps <-> ch))
eloi.3	|- (v = (1st` (2nd` A)) -> (ch <-> th))
eloi.4	|- (w = (2nd` (2nd` A)) -> (th <-> ta))

Assertion

Ref	Expression
eloi	|- (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} -> ta)

Distinct variable groups:   v,A,w,x,y,z   ph,x   ta,v,w,y,z

Proof of Theorem eloi

Step	Hyp	Ref	Expression
1		eqeq1 1481	. . . . . . 7 |- (x = A -> (x = <.<.y, z>., <.v, w>.>. <-> A = <.<.y, z>., <.v, w>.>.))
2	1	anbi1d 617	. . . . . 6 |- (x = A -> ((x = <.<.y, z>., <.v, w>.>. /\ ph) <-> (A = <.<.y, z>., <.v, w>.>. /\ ph)))
3	2	4exbidv 1283	. . . . 5 |- (x = A -> (E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph) <-> E.yE.zE.vE.w(A = <.<.y, z>., <.v, w>.>. /\ ph)))
4	3	elabg 1899	. . . 4 |- (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} -> (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> E.yE.zE.vE.w(A = <.<.y, z>., <.v, w>.>. /\ ph)))
5	4	ibi 592	. . 3 |- (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} -> E.yE.zE.vE.w(A = <.<.y, z>., <.v, w>.>. /\ ph))
6		id 59	. . . . . . . . 9 |- (A = <.<.y, z>., <.v, w>.>. -> A = <.<.y, z>., <.v, w>.>.)
7		opex 2782	. . . . . . . . . 10 |- <.y, z>. e. V
8		opex 2782	. . . . . . . . . 10 |- <.v, w>. e. V
9		opelxpi 3217	. . . . . . . . . 10 |- ((<.y, z>. e. V /\ <.v, w>. e. V) -> <.<.y, z>., <.v, w>.>. e. (V X. V))
10	7, 8, 9	mp2an 697	. . . . . . . . 9 |- <.<.y, z>., <.v, w>.>. e. (V X. V)
11	6, 10	syl6eqel 1556	. . . . . . . 8 |- (A = <.<.y, z>., <.v, w>.>. -> A e. (V X. V))
12		relxp 3255	. . . . . . . . 9 |- Rel (V X. V)
13		1st2nd 4108	. . . . . . . . 9 |- ((Rel (V X. V) /\ A e. (V X. V)) -> A = <.(1st` A), (2nd` A)>.)
14	12, 13	mpan 695	. . . . . . . 8 |- (A e. (V X. V) -> A = <.(1st` A), (2nd` A)>.)
15	11, 14	syl 10	. . . . . . 7 |- (A = <.<.y, z>., <.v, w>.>. -> A = <.(1st` A), (2nd` A)>.)
16		fveq2 3724	. . . . . . . . . . 11 |- (A = <.<.y, z>., <.v, w>.>. -> (1st` A) = (1st` <.<.y, z>., <.v, w>.>.))
17	7	op1st 4085	. . . . . . . . . . 11 |- (1st` <.<.y, z>., <.v, w>.>.) = <.y, z>.
18	16, 17	syl6eq 1523	. . . . . . . . . 10 |- (A = <.<.y, z>., <.v, w>.>. -> (1st` A) = <.y, z>.)
19		visset 1813	. . . . . . . . . . 11 |- y e. V
20		visset 1813	. . . . . . . . . . 11 |- z e. V
21		opelxpi 3217	. . . . . . . . . . 11 |- ((y e. V /\ z e. V) -> <.y, z>. e. (V X. V))
22	19, 20, 21	mp2an 697	. . . . . . . . . 10 |- <.y, z>. e. (V X. V)
23	18, 22	syl6eqel 1556	. . . . . . . . 9 |- (A = <.<.y, z>., <.v, w>.>. -> (1st` A) e. (V X. V))
24		1st2nd 4108	. . . . . . . . . 10 |- ((Rel (V X. V) /\ (1st` A) e. (V X. V)) -> (1st` A) = <.(1st` (1st` A)), (2nd` (1st` A))>.)
25	12, 24	mpan 695	. . . . . . . . 9 |- ((1st` A) e. (V X. V) -> (1st` A) = <.(1st` (1st` A)), (2nd` (1st` A))>.)
26	23, 25	syl 10	. . . . . . . 8 |- (A = <.<.y, z>., <.v, w>.>. -> (1st` A) = <.(1st` (1st` A)), (2nd` (1st` A))>.)
27		fveq2 3724	. . . . . . . . . . 11 |- (A = <.<.y, z>., <.v, w>.>. -> (2nd` A) = (2nd` <.<.y, z>., <.v, w>.>.))
28	7, 8	op2nd 4086	. . . . . . . . . . 11 |- (2nd` <.<.y, z>., <.v, w>.>.) = <.v, w>.
29	27, 28	syl6eq 1523	. . . . . . . . . 10 |- (A = <.<.y, z>., <.v, w>.>. -> (2nd` A) = <.v, w>.)
30		visset 1813	. . . . . . . . . . 11 |- v e. V
31		visset 1813	. . . . . . . . . . 11 |- w e. V
32		opelxpi 3217	. . . . . . . . . . 11 |- ((v e. V /\ w e. V) -> <.v, w>. e. (V X. V))
33	30, 31, 32	mp2an 697	. . . . . . . . . 10 |- <.v, w>. e. (V X. V)
34	29, 33	syl6eqel 1556	. . . . . . . . 9 |- (A = <.<.y, z>., <.v, w>.>. -> (2nd` A) e. (V X. V))
35		1st2nd 4108	. . . . . . . . . 10 |- ((Rel (V X. V) /\ (2nd` A) e. (V X. V)) -> (2nd` A) = <.(1st` (2nd` A)), (2nd` (2nd` A))>.)
36	12, 35	mpan 695	. . . . . . . . 9 |- ((2nd` A) e. (V X. V) -> (2nd` A) = <.(1st` (2nd` A)), (2nd` (2nd` A))>.)
37	34, 36	syl 10	. . . . . . . 8 |- (A = <.<.y, z>., <.v, w>.>. -> (2nd` A) = <.(1st` (2nd` A)), (2nd` (2nd` A))>.)
38	26, 37	opeq12d 2495	. . . . . . 7 |- (A = <.<.y, z>., <.v, w>.>. -> <.(1st` A), (2nd` A)>. = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
39	15, 38	eqtrd 1507	. . . . . 6 |- (A = <.<.y, z>., <.v, w>.>. -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
40	39	adantr 389	. . . . 5 |- ((A = <.<.y, z>., <.v, w>.>. /\ ph) -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
41	40	19.23aivv 1296	. . . 4 |- (E.vE.w(A = <.<.y, z>., <.v, w>.>. /\ ph) -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
42	41	19.23aivv 1296	. . 3 |- (E.yE.zE.vE.w(A = <.<.y, z>., <.v, w>.>. /\ ph) -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
43	5, 42	syl 10	. 2 |- (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
44		eleq1 1534	. . . 4 |- (A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>. -> (A e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
45		fvex 3732	. . . . . 6 |- (1st` (1st` A)) e. V
46		fvex 3732	. . . . . 6 |- (2nd` (1st` A)) e. V
47		fvex 3732	. . . . . 6 |- (1st` (2nd` A)) e. V
48	45, 46, 47	3pm3.2i 818	. . . . 5 |- ((1st` (1st` A)) e. V /\ (2nd` (1st` A)) e. V /\ (1st` (2nd` A)) e. V)
49		fvex 3732	. . . . 5 |- (2nd` (