Metamath Proof Explorer

Theorem bnj1379

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1379.1 
|- ( ph <-> A. f e. A Fun f )
bnj1379.2 
|- D = ( dom f i^i dom g )
bnj1379.3 
|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
bnj1379.5 
|- ( ch <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )
bnj1379.6 
|- ( th <-> ( ch /\ f e. A /\ <. x , y >. e. f ) )
bnj1379.7 
|- ( ta <-> ( th /\ g e. A /\ <. x , z >. e. g ) )
Assertion bnj1379 
|- ( ps -> Fun U. A )

Proof

Step Hyp Ref Expression
1 bnj1379.1 
 |-  ( ph <-> A. f e. A Fun f )
2 bnj1379.2 
 |-  D = ( dom f i^i dom g )
3 bnj1379.3 
 |-  ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
4 bnj1379.5 
 |-  ( ch <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )
5 bnj1379.6 
 |-  ( th <-> ( ch /\ f e. A /\ <. x , y >. e. f ) )
6 bnj1379.7 
 |-  ( ta <-> ( th /\ g e. A /\ <. x , z >. e. g ) )
7 1 bnj1095 
 |-  ( ph -> A. f ph )
8 7 nf5i 
 |-  F/ f ph
9 nfra1 
 |-  F/ f A. f e. A A. g e. A ( f |` D ) = ( g |` D )
10 8 9 nfan 
 |-  F/ f ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
11 3 10 nfxfr 
 |-  F/ f ps
12 1 bnj946 
 |-  ( ph <-> A. f ( f e. A -> Fun f ) )
13 12 biimpi 
 |-  ( ph -> A. f ( f e. A -> Fun f ) )
14 13 19.21bi 
 |-  ( ph -> ( f e. A -> Fun f ) )
15 3 14 bnj832 
 |-  ( ps -> ( f e. A -> Fun f ) )
16 funrel 
 |-  ( Fun f -> Rel f )
17 15 16 syl6 
 |-  ( ps -> ( f e. A -> Rel f ) )
18 11 17 ralrimi 
 |-  ( ps -> A. f e. A Rel f )
19 reluni 
 |-  ( Rel U. A <-> A. f e. A Rel f )
20 18 19 sylibr 
 |-  ( ps -> Rel U. A )
21 eluni2 
 |-  ( <. x , y >. e. U. A <-> E. f e. A <. x , y >. e. f )
22 21 biimpi 
 |-  ( <. x , y >. e. U. A -> E. f e. A <. x , y >. e. f )
23 22 bnj1196 
 |-  ( <. x , y >. e. U. A -> E. f ( f e. A /\ <. x , y >. e. f ) )
24 4 23 bnj836 
 |-  ( ch -> E. f ( f e. A /\ <. x , y >. e. f ) )
25 nfv 
 |-  F/ f <. x , y >. e. U. A
26 nfv 
 |-  F/ f <. x , z >. e. U. A
27 11 25 26 nf3an 
 |-  F/ f ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A )
28 4 27 nfxfr 
 |-  F/ f ch
29 28 nf5ri 
 |-  ( ch -> A. f ch )
30 24 5 29 bnj1345 
 |-  ( ch -> E. f th )
31 4 simp3bi 
 |-  ( ch -> <. x , z >. e. U. A )
32 5 31 bnj835 
 |-  ( th -> <. x , z >. e. U. A )
33 eluni2 
 |-  ( <. x , z >. e. U. A <-> E. g e. A <. x , z >. e. g )
34 33 biimpi 
 |-  ( <. x , z >. e. U. A -> E. g e. A <. x , z >. e. g )
35 34 bnj1196 
 |-  ( <. x , z >. e. U. A -> E. g ( g e. A /\ <. x , z >. e. g ) )
36 32 35 syl 
 |-  ( th -> E. g ( g e. A /\ <. x , z >. e. g ) )
37 nfv 
 |-  F/ g ph
38 nfra2w 
 |-  F/ g A. f e. A A. g e. A ( f |` D ) = ( g |` D )
39 37 38 nfan 
 |-  F/ g ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
40 3 39 nfxfr 
 |-  F/ g ps
41 nfv 
 |-  F/ g <. x , y >. e. U. A
42 nfv 
 |-  F/ g <. x , z >. e. U. A
43 40 41 42 nf3an 
 |-  F/ g ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A )
44 4 43 nfxfr 
 |-  F/ g ch
45 nfv 
 |-  F/ g f e. A
46 nfv 
 |-  F/ g <. x , y >. e. f
47 44 45 46 nf3an 
 |-  F/ g ( ch /\ f e. A /\ <. x , y >. e. f )
48 5 47 nfxfr 
 |-  F/ g th
49 48 nf5ri 
 |-  ( th -> A. g th )
50 36 6 49 bnj1345 
 |-  ( th -> E. g ta )
51 3 simprbi 
 |-  ( ps -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
52 4 51 bnj835 
 |-  ( ch -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
53 5 52 bnj835 
 |-  ( th -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
54 6 53 bnj835 
 |-  ( ta -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
55 5 6 bnj1219 
 |-  ( ta -> f e. A )
56 54 55 bnj1294 
 |-  ( ta -> A. g e. A ( f |` D ) = ( g |` D ) )
57 6 simp2bi 
 |-  ( ta -> g e. A )
58 56 57 bnj1294 
 |-  ( ta -> ( f |` D ) = ( g |` D ) )
59 58 fveq1d 
 |-  ( ta -> ( ( f |` D ) ` x ) = ( ( g |` D ) ` x ) )
60 5 simp3bi 
 |-  ( th -> <. x , y >. e. f )
61 6 60 bnj835 
 |-  ( ta -> <. x , y >. e. f )
62 vex 
 |-  x e. _V
63 vex 
 |-  y e. _V
64 62 63 opeldm 
 |-  ( <. x , y >. e. f -> x e. dom f )
65 61 64 syl 
 |-  ( ta -> x e. dom f )
66 vex 
 |-  z e. _V
67 62 66 opeldm 
 |-  ( <. x , z >. e. g -> x e. dom g )
68 6 67 bnj837 
 |-  ( ta -> x e. dom g )
69 65 68 elind 
 |-  ( ta -> x e. ( dom f i^i dom g ) )
70 69 2 eleqtrrdi 
 |-  ( ta -> x e. D )
71 70 fvresd 
 |-  ( ta -> ( ( f |` D ) ` x ) = ( f ` x ) )
72 70 fvresd 
 |-  ( ta -> ( ( g |` D ) ` x ) = ( g ` x ) )
73 59 71 72 3eqtr3d 
 |-  ( ta -> ( f ` x ) = ( g ` x ) )
74 1 biimpi 
 |-  ( ph -> A. f e. A Fun f )
75 3 74 bnj832 
 |-  ( ps -> A. f e. A Fun f )
76 4 75 bnj835 
 |-  ( ch -> A. f e. A Fun f )
77 5 76 bnj835 
 |-  ( th -> A. f e. A Fun f )
78 6 77 bnj835 
 |-  ( ta -> A. f e. A Fun f )
79 78 55 bnj1294 
 |-  ( ta -> Fun f )
80 funopfv 
 |-  ( Fun f -> ( <. x , y >. e. f -> ( f ` x ) = y ) )
81 79 61 80 sylc 
 |-  ( ta -> ( f ` x ) = y )
82 funeq 
 |-  ( f = g -> ( Fun f <-> Fun g ) )
83 82 78 57 rspcdva 
 |-  ( ta -> Fun g )
84 6 simp3bi 
 |-  ( ta -> <. x , z >. e. g )
85 funopfv 
 |-  ( Fun g -> ( <. x , z >. e. g -> ( g ` x ) = z ) )
86 83 84 85 sylc 
 |-  ( ta -> ( g ` x ) = z )
87 73 81 86 3eqtr3d 
 |-  ( ta -> y = z )
88 50 87 bnj593 
 |-  ( th -> E. g y = z )
89 88 bnj937 
 |-  ( th -> y = z )
90 30 89 bnj593 
 |-  ( ch -> E. f y = z )
91 90 bnj937 
 |-  ( ch -> y = z )
92 4 91 sylbir 
 |-  ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z )
93 92 3expib 
 |-  ( ps -> ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
94 93 alrimivv 
 |-  ( ps -> A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
95 94 alrimiv 
 |-  ( ps -> A. x A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
96 dffun4 
 |-  ( Fun U. A <-> ( Rel U. A /\ A. x A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) ) )
97 20 95 96 sylanbrc 
 |-  ( ps -> Fun U. A )