Theorem bnj1129 13425

Description: Property of trCl.

Hypotheses

Ref	Expression
bnj1129.1	|- (ph <-> (f` (/)) = pred(X, A, R))
bnj1129.2	|- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
bnj1129.3	|- D = (om \ {(/)})
bnj1129.4	|- B = {f | E.n e. D (f Fn n /\ ph /\ ps)}
bnj1129.5	|- (ch <-> (n e. D /\ f Fn n /\ ph /\ ps))

Assertion

Ref	Expression
bnj1129	|- (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))

Distinct variable groups:   A,f,i,n,y   D,i,y   R,f,i,n,y   f,X,i,n,y   f,Y,i,n,y   ph,i,y

Proof of Theorem bnj1129

Step	Hyp	Ref	Expression
1		ax-17 1317	. . . 4 |- (Y e. trCl(X, A, R) -> A.y Y e. trCl(X, A, R))
2		bnj1129.5	. . . . . . . . . 10 |- (ch <-> (n e. D /\ f Fn n /\ ph /\ ps))
3		ax-17 1317	. . . . . . . . . . 11 |- (n e. D -> A.y n e. D)
4		ax-17 1317	. . . . . . . . . . 11 |- (f Fn n -> A.y f Fn n)
5		ax-17 1317	. . . . . . . . . . 11 |- (ph -> A.yph)
6		bnj1129.2	. . . . . . . . . . . 12 |- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
7		ax-17 1317	. . . . . . . . . . . . 13 |- (i e. om -> A.y i e. om)
8		ax-17 1317	. . . . . . . . . . . . . 14 |- (suc i e. n -> A.y suc i e. n)
9		ax-17 1317	. . . . . . . . . . . . . . 15 |- (w e. (f` suc i) -> A.y w e. (f` suc i))
10		hbiu1 3281	. . . . . . . . . . . . . . 15 |- (w e. U_y e. (f` i) pred(y, A, R) -> A.y w e. U_y e. (f` i) pred(y, A, R))
11	9, 10	hbeq 1995	. . . . . . . . . . . . . 14 |- ((f` suc i) = U_y e. (f` i) pred(y, A, R) -> A.y(f` suc i) = U_y e. (f` i) pred(y, A, R))
12	8, 11	hbim 1354	. . . . . . . . . . . . 13 |- ((suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)) -> A.y(suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
13	7, 12	hbral 2146	. . . . . . . . . . . 12 |- (A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)) -> A.yA.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
14	6, 13	bnj572 12545	. . . . . . . . . . 11 |- (ps -> A.yps)
15	3, 4, 5, 14	bnj982 12864	. . . . . . . . . 10 |- ((n e. D /\ f Fn n /\ ph /\ ps) -> A.y(n e. D /\ f Fn n /\ ph /\ ps))
16	2, 15	bnj572 12545	. . . . . . . . 9 |- (ch -> A.ych)
17		ax-17 1317	. . . . . . . . 9 |- (i e. n -> A.y i e. n)
18		ax-17 1317	. . . . . . . . 9 |- (Y e. (f` i) -> A.y Y e. (f` i))
19	16, 17, 18	hb3an 1359	. . . . . . . 8 |- ((ch /\ i e. n /\ Y e. (f` i)) -> A.y(ch /\ i e. n /\ Y e. (f` i)))
20	19	hbex 1353	. . . . . . 7 |- (E.i(ch /\ i e. n /\ Y e. (f` i)) -> A.yE.i(ch /\ i e. n /\ Y e. (f` i)))
21	20	hbex 1353	. . . . . 6 |- (E.nE.i(ch /\ i e. n /\ Y e. (f` i)) -> A.yE.nE.i(ch /\ i e. n /\ Y e. (f` i)))
22	21	hbex 1353	. . . . 5 |- (E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)) -> A.yE.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))
23	1, 22	hbim 1354	. . . 4 |- ((Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i))) -> A.y(Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i))))
24	1, 23	hbim 1354	. . 3 |- ((Y e. trCl(X, A, R) -> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))) -> A.y(Y e. trCl(X, A, R) -> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))))
25		bnj1129.1	. . . . . 6 |- (ph <-> (f` (/)) = pred(X, A, R))
26		bnj1129.3	. . . . . 6 |- D = (om \ {(/)})
27		bnj1129.4	. . . . . 6 |- B = {f | E.n e. D (f Fn n /\ ph /\ ps)}
28	25, 6, 26, 27, 2	bnj917 13333	. . . . 5 |- (y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ y e. (f` i)))
29	28	a1i 8	. . . 4 |- (Y e. trCl(X, A, R) -> (y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ y e. (f` i))))
30		elex 2302	. . . . . 6 |- (Y e. trCl(X, A, R) -> E.y y = Y)
31		eleq1 1957	. . . . . . 7 |- (y = Y -> (y e. trCl(X, A, R) <-> Y e. trCl(X, A, R)))
32		eleq1 1957	. . . . . . . . . . 11 |- (y = Y -> (y e. (f` i) <-> Y e. (f` i)))
33	32	3anbi3d 1174	. . . . . . . . . 10 |- (y = Y -> ((ch /\ i e. n /\ y e. (f` i)) <-> (ch /\ i e. n /\ Y e. (f` i))))
34	33	exbidv 1657	. . . . . . . . 9 |- (y = Y -> (E.i(ch /\ i e. n /\ y e. (f` i)) <-> E.i(ch /\ i e. n /\ Y e. (f` i))))
35	34	exbidv 1657	. . . . . . . 8 |- (y = Y -> (E.nE.i(ch /\ i e. n /\ y e. (f` i)) <-> E.nE.i(ch /\ i e. n /\ Y e. (f` i))))
36	35	exbidv 1657	. . . . . . 7 |- (y = Y -> (E.fE.nE.i(ch /\ i e. n /\ y e. (f` i)) <-> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i))))
37	31, 36	imbi12d 688	. . . . . 6 |- (y = Y -> ((y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ y e. (f` i))) <-> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))))
38	30, 37	bnj593 12556	. . . . 5 |- (Y e. trCl(X, A, R) -> E.y((y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ y e. (f` i))) <-> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))))
39	38	bnj855 12788	. . . 4 |- E.y(Y e. trCl(X, A, R) -> ((y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ y e. (f` i))) <-> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))))
40	29, 39	bnj1130 12933	. . 3 |- E.y(Y e. trCl(X, A, R) -> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i))))
41	24, 40	bnj1131 12934	. 2 |- (Y e. trCl(X, A, R) -> (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i))))
42	41	pm2.43i 78	1 |- (Y e. trCl(X, A, R) -> E.fE.nE.i(ch /\ i e. n /\ Y e. (f` i)))

Syntax hints:   -> wi 3   <-> wb 163   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106   \ cdif 2590  (/)c0 2875  {csn 3044  U_ciun 3255  suc csuc 3659  omcom 3949   Fn wfn 3993  ` cfv 3998   /\ syn-bnj17 12019   predsyn-bnj14 12023   trClsyn-bnj18 12029

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-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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-iun 3257  df-fn 4009  df-bnj17 12020  df-bnj18 12030

Copyright terms: Public domain