Theorem bnj150 30946

Description: Technical lemma for bnj151 30947. 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
bnj150.1	|- ( ph <-> ( f ` (/) ) = pred ( x , A , R ) )
bnj150.2	|- ( ps <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
bnj150.3	|- ( ze <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
bnj150.4	|- ( ph' <-> [. 1o / n ]. ph )
bnj150.5	|- ( ps' <-> [. 1o / n ]. ps )
bnj150.6	|- ( th0 <-> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
bnj150.7	|- ( ze' <-> [. 1o / n ]. ze )
bnj150.8	|- F = { <. (/) , pred ( x , A , R ) >. }
bnj150.9	|- ( ph" <-> [. F / f ]. ph' )
bnj150.10	|- ( ps" <-> [. F / f ]. ps' )
bnj150.11	|- ( ze" <-> [. F / f ]. ze' )

Assertion

Ref	Expression
bnj150	|- th0

Distinct variable groups:   A, f, n, x   f, F, i, y   R, f, n, x   f, ze"   i, n, y

Allowed substitution hints:   ph( x, y, f, i, n)   ps( x, y, f, i, n)   ze( x, y, f, i, n)   A( y, i)   R( y, i)   F( x, n)   ph'( x, y, f, i, n)   ps'( x, y, f, i, n)   ze'( x, y, f, i, n)   ph"( x, y, f, i, n)   ps"( x, y, f, i, n)   ze"( x, y, i, n)   th0( x, y, f, i, n)

Proof of Theorem bnj150

Step	Hyp	Ref	Expression
1		0ex 4790	. . . . . . . . . 10 |- (/) e. _V
2		bnj93 30933	. . . . . . . . . 10 |- ( ( R FrSe A /\ x e. A ) -> pred ( x , A , R ) e. _V )
3		funsng 5937	. . . . . . . . . 10 |- ( ( (/) e. _V /\ pred ( x , A , R ) e. _V ) -> Fun { <. (/) , pred ( x , A , R ) >. } )
4	1, 2, 3	sylancr 695	. . . . . . . . 9 |- ( ( R FrSe A /\ x e. A ) -> Fun { <. (/) , pred ( x , A , R ) >. } )
5		bnj150.8	. . . . . . . . . 10 |- F = { <. (/) , pred ( x , A , R ) >. }
6	5	funeqi 5909	. . . . . . . . 9 |- ( Fun F <-> Fun { <. (/) , pred ( x , A , R ) >. } )
7	4, 6	sylibr 224	. . . . . . . 8 |- ( ( R FrSe A /\ x e. A ) -> Fun F )
8	5	bnj96 30935	. . . . . . . 8 |- ( ( R FrSe A /\ x e. A ) -> dom F = 1o )
9	7, 8	bnj1422 30908	. . . . . . 7 |- ( ( R FrSe A /\ x e. A ) -> F Fn 1o )
10	5	bnj97 30936	. . . . . . . 8 |- ( ( R FrSe A /\ x e. A ) -> ( F ` (/) ) = pred ( x , A , R ) )
11		bnj150.1	. . . . . . . . 9 |- ( ph <-> ( f ` (/) ) = pred ( x , A , R ) )
12		bnj150.4	. . . . . . . . 9 |- ( ph' <-> [. 1o / n ]. ph )
13		bnj150.9	. . . . . . . . 9 |- ( ph" <-> [. F / f ]. ph' )
14	11, 12, 13, 5	bnj125 30942	. . . . . . . 8 |- ( ph" <-> ( F ` (/) ) = pred ( x , A , R ) )
15	10, 14	sylibr 224	. . . . . . 7 |- ( ( R FrSe A /\ x e. A ) -> ph" )
16	9, 15	jca 554	. . . . . 6 |- ( ( R FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) )
17		bnj98 30937	. . . . . . 7 |- A. i e. om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) )
18		bnj150.2	. . . . . . . 8 |- ( ps <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
19		bnj150.5	. . . . . . . 8 |- ( ps' <-> [. 1o / n ]. ps )
20		bnj150.10	. . . . . . . 8 |- ( ps" <-> [. F / f ]. ps' )
21	18, 19, 20, 5	bnj126 30943	. . . . . . 7 |- ( ps" <-> A. i e. om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) ) )
22	17, 21	mpbir 221	. . . . . 6 |- ps"
23	16, 22	jctir 561	. . . . 5 |- ( ( R FrSe A /\ x e. A ) -> ( ( F Fn 1o /\ ph" ) /\ ps" ) )
24		df-3an 1039	. . . . 5 |- ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) )
25	23, 24	sylibr 224	. . . 4 |- ( ( R FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) )
26		bnj150.11	. . . . 5 |- ( ze" <-> [. F / f ]. ze' )
27		bnj150.3	. . . . . 6 |- ( ze <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )
28		bnj150.7	. . . . . 6 |- ( ze' <-> [. 1o / n ]. ze )
29	27, 28, 12, 19	bnj121 30940	. . . . 5 |- ( ze' <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
30	5, 13, 20, 26, 29	bnj124 30941	. . . 4 |- ( ze" <-> ( ( R FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )
31	25, 30	mpbir 221	. . 3 |- ze"
32	5	bnj95 30934	. . . 4 |- F e. _V
33		sbceq1a 3446	. . . . 5 |- ( f = F -> ( ze' <-> [. F / f ]. ze' ) )
34	33, 26	syl6bbr 278	. . . 4 |- ( f = F -> ( ze' <-> ze" ) )
35	32, 34	spcev 3300	. . 3 |- ( ze" -> E. f ze' )
36	31, 35	ax-mp 5	. 2 |- E. f ze'
37		bnj150.6	. . . 4 |- ( th0 <-> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
38		19.37v 1910	. . . 4 |- ( E. f ( ( R FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )
39	37, 38	bitr4i 267	. . 3 |- ( th0 <-> E. f ( ( R FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
40	39, 29	bnj133 30793	. 2 |- ( th0 <-> E. f ze' )
41	36, 40	mpbir 221	1 |- th0

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   _Vcvv 3200   [.wsbc 3435   (/)c0 3915   {csn 4177   <.cop 4183   U_ciun 4520   suc csuc 5725   Fun wfun 5882   Fn wfn 5883   ` cfv 5888   omcom 7065   1oc1o 7553   predc-bnj14 30754   FrSe w-bnj15 30758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-1o 7560  df-bnj13 30757  df-bnj15 30759

This theorem is referenced by:  bnj151  30947