Theorem elo 14342

Description: The law of concretion for operation class abstraction. Compare with eloprabg 4936. This version is to be used with categories.

Hypotheses

Ref	Expression
elo.1	|- (y = A -> (ph <-> ps))
elo.2	|- (z = B -> (ps <-> ch))
elo.3	|- (v = C -> (ch <-> th))
elo.4	|- (w = D -> (th <-> ta))

Assertion

Ref	Expression
elo	|- (((A e. Q /\ B e. R /\ C e. S) /\ D e. T) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))

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

Proof of Theorem elo

Step	Hyp	Ref	Expression
1		opex 3527	. . 3 |- <.<.A, B>., <.C, D>.>. e. _V
2		eqeq1 1890	. . . . . . . . . 10 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>.))
3		eqcom 1886	. . . . . . . . . 10 |- (<.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.)
4	2, 3	syl6bb 595	. . . . . . . . 9 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.))
5		simpl2 880	. . . . . . . . . 10 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> B e. _V)
6		opelxpi 4040	. . . . . . . . . . 11 |- ((C e. _V /\ D e. _V) -> <.C, D>. e. (_V X. _V))
7	6	3ad2antl3 1040	. . . . . . . . . 10 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> <.C, D>. e. (_V X. _V))
8		simpr 350	. . . . . . . . . 10 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> D e. _V)
9		visset 2295	. . . . . . . . . . . . 13 |- y e. _V
10		visset 2295	. . . . . . . . . . . . 13 |- z e. _V
11		opex 3527	. . . . . . . . . . . . 13 |- <.v, w>. e. _V
12	9, 10, 11	otthg 3535	. . . . . . . . . . . 12 |- ((B e. _V /\ <.C, D>. e. (_V X. _V)) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> (y = A /\ z = B /\ <.v, w>. = <.C, D>.)))
13	12	3adant3 896	. . . . . . . . . . 11 |- ((B e. _V /\ <.C, D>. e. (_V X. _V) /\ D e. _V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> (y = A /\ z = B /\ <.v, w>. = <.C, D>.)))
14		visset 2295	. . . . . . . . . . . . . . 15 |- v e. _V
15		visset 2295	. . . . . . . . . . . . . . 15 |- w e. _V
16	14, 15	opthg 3533	. . . . . . . . . . . . . 14 |- (D e. _V -> (<.v, w>. = <.C, D>. <-> (v = C /\ w = D)))
17	16	3anbi3d 1174	. . . . . . . . . . . . 13 |- (D e. _V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> (y = A /\ z = B /\ (v = C /\ w = D))))
18		and4as 14266	. . . . . . . . . . . . 13 |- ((y = A /\ z = B /\ (v = C /\ w = D)) <-> ((y = A /\ z = B /\ v = C) /\ w = D))
19	17, 18	syl6bb 595	. . . . . . . . . . . 12 |- (D e. _V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
20	19	3ad2ant3 899	. . . . . . . . . . 11 |- ((B e. _V /\ <.C, D>. e. (_V X. _V) /\ D e. _V) -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
21	13, 20	bitrd 587	. . . . . . . . . 10 |- ((B e. _V /\ <.C, D>. e. (_V X. _V) /\ D e. _V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
22	5, 7, 8, 21	syl111anc 1100	. . . . . . . . 9 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
23	4, 22	sylan9bbr 600	. . . . . . . 8 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> (u = <.<.y, z>., <.v, w>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
24	23	anbi1d 679	. . . . . . 7 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> ((u = <.<.y, z>., <.v, w>.>. /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ph)))
25		elo.1	. . . . . . . . . 10 |- (y = A -> (ph <-> ps))
26		elo.2	. . . . . . . . . 10 |- (z = B -> (ps <-> ch))
27		elo.3	. . . . . . . . . 10 |- (v = C -> (ch <-> th))
28	25, 26, 27	syl3an9b 1166	. . . . . . . . 9 |- ((y = A /\ z = B /\ v = C) -> (ph <-> th))
29		elo.4	. . . . . . . . 9 |- (w = D -> (th <-> ta))
30	28, 29	sylan9bb 599	. . . . . . . 8 |- (((y = A /\ z = B /\ v = C) /\ w = D) -> (ph <-> ta))
31	30	pm5.32i 707	. . . . . . 7 |- ((((y = A /\ z = B /\ v = C) /\ w = D) /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ta))
32	24, 31	syl6bb 595	. . . . . 6 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> ((u = <.<.y, z>., <.v, w>.>. /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ta)))
33	32	4exbidv 1661	. . . . 5 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> E.yE.zE.vE.w(((y = A /\ z = B /\ v = C) /\ w = D) /\ ta)))
34		eleq1 1957	. . . . . . 7 |- (u = <.<.A, B>., <.C, D>.>. -> (u e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> <.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
35		visset 2295	. . . . . . . 8 |- u e. _V
36		eqeq1 1890	. . . . . . . . . 10 |- (x = u -> (x = <.<.y, z>., <.v, w>.>. <-> u = <.<.y, z>., <.v, w>.>.))
37	36	anbi1d 679	. . . . . . . . 9 |- (x = u -> ((x = <.<.y, z>., <.v, w>.>. /\ ph) <-> (u = <.<.y, z>., <.v, w>.>. /\ ph)))
38	37	4exbidv 1661	. . . . . . . 8 |- (x = u -> (E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph) <-> E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph)))
39	35, 38	elab 2403	. . . . . . 7 |- (u e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph))
40	34, 39	syl5bbr 593	. . . . . 6 |- (u = <.<.A, B>., <.C, D>.>. -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> <.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
41	40	adantl 424	. . . . 5 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> <.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
42		elex 2302	. . . . . . . . . . 11 |- (A e. _V -> E.y y = A)
43		elex 2302	. . . . . . . . . . 11 |- (B e. _V -> E.z z = B)
44		elex 2302	. . . . . . . . . . 11 |- (C e. _V -> E.v v = C)
45	42, 43, 44	3anim123i 1053	. . . . . . . . . 10 |- ((A e. _V /\ B e. _V /\ C e. _V) -> (E.y y = A /\ E.z z = B /\ E.v v = C))
46		elex 2302	. . . . . . . . . 10 |- (D e. _V -> E.w w = D)
47	45, 46	anim12i 360	. . . . . . . . 9 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> ((E.y y = A /\ E.z z = B /\ E.v v = C) /\ E.w w = D))
48		eeeeanv 14272	. . . . . . . . 9 |- (E.yE.zE.vE.w((y = A /\ z = B /\ v = C) /\ w = D) <-> ((E.y y = A /\ E.z z = B /\ E.v v = C) /\ E.w w = D))
49	47, 48	sylibr 217	. . . . . . . 8 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> E.yE.zE.vE.w((y = A /\ z = B /\ v = C) /\ w = D))
50	49	biantrurd 796	. . . . . . 7 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> (ta <-> (E.yE.zE.vE.w((y = A /\ z = B /\ v = C) /\ w = D) /\ ta)))
51		19.41vvvv 14271	. . . . . . 7 |- (E.yE.zE.vE.w(((y = A /\ z = B /\ v = C) /\ w = D) /\ ta) <-> (E.yE.zE.vE.w((y = A /\ z = B /\ v = C) /\ w = D) /\ ta))
52	50, 51	syl6rbbr 598	. . . . . 6 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> (E.yE.zE.vE.w(((y = A /\ z = B /\ v = C) /\ w = D) /\ ta) <-> ta))
53	52	adantr 425	. . . . 5 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> (E.yE.zE.vE.w(((y = A /\ z = B /\ v = C) /\ w = D) /\ ta) <-> ta))
54	33, 41, 53	3bitr3d 607	. . . 4 |- ((((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) /\ u = <.<.A, B>., <.C, D>.>.) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))
55	54	expcom 403	. . 3 |- (u = <.<.A, B>., <.C, D>.>. -> (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta)))
56	1, 55	vtocle 2359	. 2 |- (((A e. _V /\ B e. _V /\ C e. _V) /\ D e. _V) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))
57		elisset 2299	. . 3 |- (A e. Q -> A e. _V)
58		elisset 2299	. . 3 |- (B e. R -> B e. _V)
59		elisset 2299	. . 3 |- (C e. S -> C e. _V)
60	57, 58, 59	3anim123i 1053	. 2 |- ((A e. Q /\ B e. R /\ C e. S) -> (A e. _V /\ B e. _V /\ C e. _V))
61		elisset 2299	. 2 |- (D e. T -> D e. _V)
62	56, 60, 61	syl2an 503	1 |- (((A e. Q /\ B e. R /\ C e. S) /\ D e. T) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  _Vcvv 2292  <.cop 3046   X. cxp 3984

This theorem is referenced by:  eloi 14400  vecval1b 14794  isalg 15068  isded 15083  iscat 15101

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-opab 3396  df-xp 4000

Copyright terms: Public domain