Metamath Proof Explorer

Theorem bnj1501

Description: Technical lemma for bnj1500 . 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 bnj1501.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1501.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1501.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1501.4 
|- F = U. C
bnj1501.5 
|- ( ph <-> ( R _FrSe A /\ x e. A ) )
bnj1501.6 
|- ( ps <-> ( ph /\ f e. C /\ x e. dom f ) )
bnj1501.7 
|- ( ch <-> ( ps /\ d e. B /\ dom f = d ) )
Assertion bnj1501 
|- ( R _FrSe A -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )

Proof

Step Hyp Ref Expression
1 bnj1501.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1501.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1501.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1501.4 
 |-  F = U. C
5 bnj1501.5 
 |-  ( ph <-> ( R _FrSe A /\ x e. A ) )
6 bnj1501.6 
 |-  ( ps <-> ( ph /\ f e. C /\ x e. dom f ) )
7 bnj1501.7 
 |-  ( ch <-> ( ps /\ d e. B /\ dom f = d ) )
8 5 simprbi 
 |-  ( ph -> x e. A )
9 1 2 3 4 bnj60 
 |-  ( R _FrSe A -> F Fn A )
10 9 fndmd 
 |-  ( R _FrSe A -> dom F = A )
11 5 10 bnj832 
 |-  ( ph -> dom F = A )
12 8 11 eleqtrrd 
 |-  ( ph -> x e. dom F )
13 4 dmeqi 
 |-  dom F = dom U. C
14 3 bnj1317 
 |-  ( w e. C -> A. f w e. C )
15 14 bnj1400 
 |-  dom U. C = U_ f e. C dom f
16 13 15 eqtri 
 |-  dom F = U_ f e. C dom f
17 12 16 eleqtrdi 
 |-  ( ph -> x e. U_ f e. C dom f )
18 17 bnj1405 
 |-  ( ph -> E. f e. C x e. dom f )
19 18 6 bnj1209 
 |-  ( ph -> E. f ps )
20 3 bnj1436 
 |-  ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
21 20 bnj1299 
 |-  ( f e. C -> E. d e. B f Fn d )
22 fndm 
 |-  ( f Fn d -> dom f = d )
23 21 22 bnj31 
 |-  ( f e. C -> E. d e. B dom f = d )
24 6 23 bnj836 
 |-  ( ps -> E. d e. B dom f = d )
25 1 2 3 4 5 6 bnj1518 
 |-  ( ps -> A. d ps )
26 24 7 25 bnj1521 
 |-  ( ps -> E. d ch )
27 9 fnfund 
 |-  ( R _FrSe A -> Fun F )
28 5 27 bnj832 
 |-  ( ph -> Fun F )
29 6 28 bnj835 
 |-  ( ps -> Fun F )
30 elssuni 
 |-  ( f e. C -> f C_ U. C )
31 30 4 sseqtrrdi 
 |-  ( f e. C -> f C_ F )
32 6 31 bnj836 
 |-  ( ps -> f C_ F )
33 6 simp3bi 
 |-  ( ps -> x e. dom f )
34 29 32 33 bnj1502 
 |-  ( ps -> ( F ` x ) = ( f ` x ) )
35 1 2 3 bnj1514 
 |-  ( f e. C -> A. x e. dom f ( f ` x ) = ( G ` Y ) )
36 6 35 bnj836 
 |-  ( ps -> A. x e. dom f ( f ` x ) = ( G ` Y ) )
37 36 33 bnj1294 
 |-  ( ps -> ( f ` x ) = ( G ` Y ) )
38 34 37 eqtrd 
 |-  ( ps -> ( F ` x ) = ( G ` Y ) )
39 7 38 bnj835 
 |-  ( ch -> ( F ` x ) = ( G ` Y ) )
40 7 29 bnj835 
 |-  ( ch -> Fun F )
41 7 32 bnj835 
 |-  ( ch -> f C_ F )
42 1 bnj1517 
 |-  ( d e. B -> A. x e. d _pred ( x , A , R ) C_ d )
43 7 42 bnj836 
 |-  ( ch -> A. x e. d _pred ( x , A , R ) C_ d )
44 7 33 bnj835 
 |-  ( ch -> x e. dom f )
45 7 simp3bi 
 |-  ( ch -> dom f = d )
46 44 45 eleqtrd 
 |-  ( ch -> x e. d )
47 43 46 bnj1294 
 |-  ( ch -> _pred ( x , A , R ) C_ d )
48 47 45 sseqtrrd 
 |-  ( ch -> _pred ( x , A , R ) C_ dom f )
49 40 41 48 bnj1503 
 |-  ( ch -> ( F |` _pred ( x , A , R ) ) = ( f |` _pred ( x , A , R ) ) )
50 49 opeq2d 
 |-  ( ch -> <. x , ( F |` _pred ( x , A , R ) ) >. = <. x , ( f |` _pred ( x , A , R ) ) >. )
51 50 2 eqtr4di 
 |-  ( ch -> <. x , ( F |` _pred ( x , A , R ) ) >. = Y )
52 51 fveq2d 
 |-  ( ch -> ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) = ( G ` Y ) )
53 39 52 eqtr4d 
 |-  ( ch -> ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
54 26 53 bnj593 
 |-  ( ps -> E. d ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
55 1 2 3 4 bnj1519 
 |-  ( ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) -> A. d ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
56 54 55 bnj1397 
 |-  ( ps -> ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
57 19 56 bnj593 
 |-  ( ph -> E. f ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
58 1 2 3 4 bnj1520 
 |-  ( ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) -> A. f ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
59 57 58 bnj1397 
 |-  ( ph -> ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
60 5 59 bnj1459 
 |-  ( R _FrSe A -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )