Metamath Proof Explorer

Theorem bnj1384

Description: Technical lemma for bnj60 . 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.)

Ref Expression
Hypotheses bnj1384.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1384.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1384.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1384.4 
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
bnj1384.5 
|- D = { x e. A | -. E. f ta }
bnj1384.6 
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
bnj1384.7 
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
bnj1384.8 
|- ( ta' <-> [. y / x ]. ta )
bnj1384.9 
|- H = { f | E. y e. _pred ( x , A , R ) ta' }
bnj1384.10 
|- P = U. H
Assertion bnj1384 
|- ( R _FrSe A -> Fun P )

Proof

Step Hyp Ref Expression
1 bnj1384.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1384.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1384.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1384.4 
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 bnj1384.5 
 |-  D = { x e. A | -. E. f ta }
6 bnj1384.6 
 |-  ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7 bnj1384.7 
 |-  ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8 bnj1384.8 
 |-  ( ta' <-> [. y / x ]. ta )
9 bnj1384.9 
 |-  H = { f | E. y e. _pred ( x , A , R ) ta' }
10 bnj1384.10 
 |-  P = U. H
11 1 2 3 4 8 bnj1373 
 |-  ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
12 1 2 3 4 5 6 7 8 9 10 11 bnj1371 
 |-  ( f e. H -> Fun f )
13 12 rgen 
 |-  A. f e. H Fun f
14 id 
 |-  ( R _FrSe A -> R _FrSe A )
15 1 2 3 4 5 6 7 8 9 bnj1374 
 |-  ( f e. H -> f e. C )
16 nfab1 
 |-  F/_ f { f | E. y e. _pred ( x , A , R ) ta' }
17 9 16 nfcxfr 
 |-  F/_ f H
18 17 nfcri 
 |-  F/ f g e. H
19 nfab1 
 |-  F/_ f { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
20 3 19 nfcxfr 
 |-  F/_ f C
21 20 nfcri 
 |-  F/ f g e. C
22 18 21 nfim 
 |-  F/ f ( g e. H -> g e. C )
23 eleq1w 
 |-  ( f = g -> ( f e. H <-> g e. H ) )
24 eleq1w 
 |-  ( f = g -> ( f e. C <-> g e. C ) )
25 23 24 imbi12d 
 |-  ( f = g -> ( ( f e. H -> f e. C ) <-> ( g e. H -> g e. C ) ) )
26 22 25 15 chvarfv 
 |-  ( g e. H -> g e. C )
27 eqid 
 |-  ( dom f i^i dom g ) = ( dom f i^i dom g )
28 1 2 3 27 bnj1326 
 |-  ( ( R _FrSe A /\ f e. C /\ g e. C ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
29 14 15 26 28 syl3an 
 |-  ( ( R _FrSe A /\ f e. H /\ g e. H ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
30 29 3expib 
 |-  ( R _FrSe A -> ( ( f e. H /\ g e. H ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) ) )
31 30 ralrimivv 
 |-  ( R _FrSe A -> A. f e. H A. g e. H ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
32 biid 
 |-  ( A. f e. H Fun f <-> A. f e. H Fun f )
33 biid 
 |-  ( ( A. f e. H Fun f /\ A. f e. H A. g e. H ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) ) <-> ( A. f e. H Fun f /\ A. f e. H A. g e. H ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) ) )
34 9 bnj1317 
 |-  ( z e. H -> A. f z e. H )
35 32 27 33 34 bnj1386 
 |-  ( ( A. f e. H Fun f /\ A. f e. H A. g e. H ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) ) -> Fun U. H )
36 13 31 35 sylancr 
 |-  ( R _FrSe A -> Fun U. H )
37 10 funeqi 
 |-  ( Fun P <-> Fun U. H )
38 36 37 sylibr 
 |-  ( R _FrSe A -> Fun P )