Metamath Proof Explorer

Theorem bnj1321

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 bnj1321.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1321.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1321.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1321.4 
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
Assertion bnj1321 
|- ( ( R _FrSe A /\ E. f ta ) -> E! f ta )

Proof

Step Hyp Ref Expression
1 bnj1321.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1321.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1321.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1321.4 
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 simpr 
 |-  ( ( R _FrSe A /\ E. f ta ) -> E. f ta )
6 simp1 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> R _FrSe A )
7 4 simplbi 
 |-  ( ta -> f e. C )
8 7 3ad2ant2 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> f e. C )
9 nfab1 
 |-  F/_ f { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
10 3 9 nfcxfr 
 |-  F/_ f C
11 10 nfcri 
 |-  F/ f g e. C
12 nfv 
 |-  F/ f dom g = ( { x } u. _trCl ( x , A , R ) )
13 11 12 nfan 
 |-  F/ f ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) )
14 eleq1w 
 |-  ( f = g -> ( f e. C <-> g e. C ) )
15 dmeq 
 |-  ( f = g -> dom f = dom g )
16 15 eqeq1d 
 |-  ( f = g -> ( dom f = ( { x } u. _trCl ( x , A , R ) ) <-> dom g = ( { x } u. _trCl ( x , A , R ) ) ) )
17 14 16 anbi12d 
 |-  ( f = g -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) ) )
18 4 17 bitrid 
 |-  ( f = g -> ( ta <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) ) )
19 13 18 sbiev 
 |-  ( [ g / f ] ta <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) )
20 19 simplbi 
 |-  ( [ g / f ] ta -> g e. C )
21 20 3ad2ant3 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> g e. C )
22 eqid 
 |-  ( dom f i^i dom g ) = ( dom f i^i dom g )
23 1 2 3 22 bnj1326 
 |-  ( ( R _FrSe A /\ f e. C /\ g e. C ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
24 6 8 21 23 syl3anc 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
25 4 simprbi 
 |-  ( ta -> dom f = ( { x } u. _trCl ( x , A , R ) ) )
26 25 3ad2ant2 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom f = ( { x } u. _trCl ( x , A , R ) ) )
27 19 simprbi 
 |-  ( [ g / f ] ta -> dom g = ( { x } u. _trCl ( x , A , R ) ) )
28 27 3ad2ant3 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom g = ( { x } u. _trCl ( x , A , R ) ) )
29 26 28 eqtr4d 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom f = dom g )
30 bnj1322 
 |-  ( dom f = dom g -> ( dom f i^i dom g ) = dom f )
31 30 reseq2d 
 |-  ( dom f = dom g -> ( f |` ( dom f i^i dom g ) ) = ( f |` dom f ) )
32 29 31 syl 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = ( f |` dom f ) )
33 releq 
 |-  ( z = f -> ( Rel z <-> Rel f ) )
34 1 2 3 bnj66 
 |-  ( z e. C -> Rel z )
35 33 34 vtoclga 
 |-  ( f e. C -> Rel f )
36 resdm 
 |-  ( Rel f -> ( f |` dom f ) = f )
37 8 35 36 3syl 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` dom f ) = f )
38 32 37 eqtrd 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = f )
39 eqeq2 
 |-  ( dom f = dom g -> ( ( dom f i^i dom g ) = dom f <-> ( dom f i^i dom g ) = dom g ) )
40 30 39 mpbid 
 |-  ( dom f = dom g -> ( dom f i^i dom g ) = dom g )
41 40 reseq2d 
 |-  ( dom f = dom g -> ( g |` ( dom f i^i dom g ) ) = ( g |` dom g ) )
42 29 41 syl 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` ( dom f i^i dom g ) ) = ( g |` dom g ) )
43 1 2 3 bnj66 
 |-  ( g e. C -> Rel g )
44 resdm 
 |-  ( Rel g -> ( g |` dom g ) = g )
45 21 43 44 3syl 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` dom g ) = g )
46 42 45 eqtrd 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` ( dom f i^i dom g ) ) = g )
47 24 38 46 3eqtr3d 
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> f = g )
48 47 3expib 
 |-  ( R _FrSe A -> ( ( ta /\ [ g / f ] ta ) -> f = g ) )
49 48 alrimivv 
 |-  ( R _FrSe A -> A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) )
50 49 adantr 
 |-  ( ( R _FrSe A /\ E. f ta ) -> A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) )
51 nfv 
 |-  F/ g ta
52 51 eu2 
 |-  ( E! f ta <-> ( E. f ta /\ A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) ) )
53 5 50 52 sylanbrc 
 |-  ( ( R _FrSe A /\ E. f ta ) -> E! f ta )