Theorem bnj1014 31958

Description: Technical lemma for bnj69 32006. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj1014.1	|- ( ph <-> ( f ` (/) ) = pred ( X , A , R ) )
bnj1014.2	|- ( ps <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
bnj1014.13	|- D = ( om \ { (/) } )
bnj1014.14	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }

Assertion

Ref	Expression
bnj1014	|- ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) )

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

Allowed substitution hints:   ph( y, f, g, j, n)   ps( y, f, g, i, j, n)   A( g, j)   B( y, f, g, i, j, n)   D( y, f, g, j, n)   R( g, j)   X( g, j)

Proof of Theorem bnj1014

Step	Hyp	Ref	Expression
1		bnj1014.14	. . . . . . 7 |- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
2		nfcv 2584	. . . . . . . . 9 |- F/_ i D
3		bnj1014.1	. . . . . . . . . . 11 |- ( ph <-> ( f ` (/) ) = pred ( X , A , R ) )
4		bnj1014.2	. . . . . . . . . . 11 |- ( ps <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
5	3, 4	bnj911 31930	. . . . . . . . . 10 |- ( ( f Fn n /\ ph /\ ps ) -> A. i ( f Fn n /\ ph /\ ps ) )
6	5	nfi 1596	. . . . . . . . 9 |- F/ i ( f Fn n /\ ph /\ ps )
7	2, 6	nfrex 2776	. . . . . . . 8 |- F/ i E. n e. D ( f Fn n /\ ph /\ ps )
8	7	nfab 2588	. . . . . . 7 |- F/_ i { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
9	1, 8	nfcxfr 2581	. . . . . 6 |- F/_ i B
10	9	nfcri 2578	. . . . 5 |- F/ i g e. B
11		nfv 1673	. . . . 5 |- F/ i j e. dom g
12	10, 11	nfan 1861	. . . 4 |- F/ i ( g e. B /\ j e. dom g )
13		nfv 1673	. . . 4 |- F/ i ( g ` j ) C_ trCl ( X , A , R )
14	12, 13	nfim 1853	. . 3 |- F/ i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) )
15	14	nfri 1808	. 2 |- ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) ) -> A. i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) ) )
16		ax6ev 1710	. . 3 |- E. i i = j
17	1	bnj1317 31820	. . . . . . . 8 |- ( g e. B -> A. f g e. B )
18	17	nfi 1596	. . . . . . 7 |- F/ f g e. B
19		nfv 1673	. . . . . . 7 |- F/ f i e. dom g
20	18, 19	nfan 1861	. . . . . 6 |- F/ f ( g e. B /\ i e. dom g )
21		nfv 1673	. . . . . 6 |- F/ f ( g ` i ) C_ trCl ( X , A , R )
22	20, 21	nfim 1853	. . . . 5 |- F/ f ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ trCl ( X , A , R ) )
23		eleq1 2503	. . . . . . 7 |- ( f = g -> ( f e. B <-> g e. B ) )
24		dmeq 5045	. . . . . . . 8 |- ( f = g -> dom f = dom g )
25	24	eleq2d 2510	. . . . . . 7 |- ( f = g -> ( i e. dom f <-> i e. dom g ) )
26	23, 25	anbi12d 710	. . . . . 6 |- ( f = g -> ( ( f e. B /\ i e. dom f ) <-> ( g e. B /\ i e. dom g ) ) )
27		fveq1 5695	. . . . . . 7 |- ( f = g -> ( f ` i ) = ( g ` i ) )
28	27	sseq1d 3388	. . . . . 6 |- ( f = g -> ( ( f ` i ) C_ trCl ( X , A , R ) <-> ( g ` i ) C_ trCl ( X , A , R ) ) )
29	26, 28	imbi12d 320	. . . . 5 |- ( f = g -> ( ( ( f e. B /\ i e. dom f ) -> ( f ` i ) C_ trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ trCl ( X , A , R ) ) ) )
30		ssiun2 4218	. . . . . 6 |- ( i e. dom f -> ( f ` i ) C_ U_ i e. dom f ( f ` i ) )
31		ssiun2 4218	. . . . . . 7 |- ( f e. B -> U_ i e. dom f ( f ` i ) C_ U_ f e. B U_ i e. dom f ( f ` i ) )
32		bnj1014.13	. . . . . . . 8 |- D = ( om \ { (/) } )
33	3, 4, 32, 1	bnj882 31924	. . . . . . 7 |- trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )
34	31, 33	syl6sseqr 3408	. . . . . 6 |- ( f e. B -> U_ i e. dom f ( f ` i ) C_ trCl ( X , A , R ) )
35	30, 34	sylan9ssr 3375	. . . . 5 |- ( ( f e. B /\ i e. dom f ) -> ( f ` i ) C_ trCl ( X , A , R ) )
36	22, 29, 35	chvar 1957	. . . 4 |- ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ trCl ( X , A , R ) )
37		eleq1 2503	. . . . . . 7 |- ( j = i -> ( j e. dom g <-> i e. dom g ) )
38	37	anbi2d 703	. . . . . 6 |- ( j = i -> ( ( g e. B /\ j e. dom g ) <-> ( g e. B /\ i e. dom g ) ) )
39		fveq2 5696	. . . . . . 7 |- ( j = i -> ( g ` j ) = ( g ` i ) )
40	39	sseq1d 3388	. . . . . 6 |- ( j = i -> ( ( g ` j ) C_ trCl ( X , A , R ) <-> ( g ` i ) C_ trCl ( X , A , R ) ) )
41	38, 40	imbi12d 320	. . . . 5 |- ( j = i -> ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ trCl ( X , A , R ) ) ) )
42	41	equcoms 1733	. . . 4 |- ( i = j -> ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ trCl ( X , A , R ) ) ) )
43	36, 42	mpbiri 233	. . 3 |- ( i = j -> ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) ) )
44	16, 43	bnj101 31717	. 2 |- E. i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) )
45	15, 44	bnj1131 31786	1 |- ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ trCl ( X , A , R ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   {cab 2429   A.wral 2720   E.wrex 2721   \ cdif 3330   C_ wss 3333   (/)c0 3642   {csn 3882   U_ciun 4176   suc csuc 4726   dom cdm 4845   Fn wfn 5418   ` cfv 5423   omcom 6481   predc-bnj14 31681   trClc-bnj18 31687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-dm 4855  df-iota 5386  df-fv 5431  df-bnj18 31688

This theorem is referenced by:  bnj1015  31959