Metamath Proof Explorer

Theorem bnj1385

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

Ref Expression
Hypotheses bnj1385.1 
|- ( ph <-> A. f e. A Fun f )
bnj1385.2 
|- D = ( dom f i^i dom g )
bnj1385.3 
|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
bnj1385.4 
|- ( x e. A -> A. f x e. A )
bnj1385.5 
|- ( ph' <-> A. h e. A Fun h )
bnj1385.6 
|- E = ( dom h i^i dom g )
bnj1385.7 
|- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) )
Assertion bnj1385 
|- ( ps -> Fun U. A )

Proof

Step Hyp Ref Expression
1 bnj1385.1 
 |-  ( ph <-> A. f e. A Fun f )
2 bnj1385.2 
 |-  D = ( dom f i^i dom g )
3 bnj1385.3 
 |-  ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
4 bnj1385.4 
 |-  ( x e. A -> A. f x e. A )
5 bnj1385.5 
 |-  ( ph' <-> A. h e. A Fun h )
6 bnj1385.6 
 |-  E = ( dom h i^i dom g )
7 bnj1385.7 
 |-  ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) )
8 nfv 
 |-  F/ h ( f e. A -> Fun f )
9 4 nfcii 
 |-  F/_ f A
10 9 nfcri 
 |-  F/ f h e. A
11 nfv 
 |-  F/ f Fun h
12 10 11 nfim 
 |-  F/ f ( h e. A -> Fun h )
13 eleq1w 
 |-  ( f = h -> ( f e. A <-> h e. A ) )
14 funeq 
 |-  ( f = h -> ( Fun f <-> Fun h ) )
15 13 14 imbi12d 
 |-  ( f = h -> ( ( f e. A -> Fun f ) <-> ( h e. A -> Fun h ) ) )
16 8 12 15 cbvalv1 
 |-  ( A. f ( f e. A -> Fun f ) <-> A. h ( h e. A -> Fun h ) )
17 df-ral 
 |-  ( A. f e. A Fun f <-> A. f ( f e. A -> Fun f ) )
18 df-ral 
 |-  ( A. h e. A Fun h <-> A. h ( h e. A -> Fun h ) )
19 16 17 18 3bitr4i 
 |-  ( A. f e. A Fun f <-> A. h e. A Fun h )
20 19 1 5 3bitr4i 
 |-  ( ph <-> ph' )
21 nfv 
 |-  F/ h ( f e. A -> A. g e. A ( f |` D ) = ( g |` D ) )
22 nfv 
 |-  F/ f ( h |` E ) = ( g |` E )
23 9 22 nfralw 
 |-  F/ f A. g e. A ( h |` E ) = ( g |` E )
24 10 23 nfim 
 |-  F/ f ( h e. A -> A. g e. A ( h |` E ) = ( g |` E ) )
25 dmeq 
 |-  ( f = h -> dom f = dom h )
26 25 ineq1d 
 |-  ( f = h -> ( dom f i^i dom g ) = ( dom h i^i dom g ) )
27 26 2 6 3eqtr4g 
 |-  ( f = h -> D = E )
28 27 reseq2d 
 |-  ( f = h -> ( f |` D ) = ( f |` E ) )
29 reseq1 
 |-  ( f = h -> ( f |` E ) = ( h |` E ) )
30 28 29 eqtrd 
 |-  ( f = h -> ( f |` D ) = ( h |` E ) )
31 27 reseq2d 
 |-  ( f = h -> ( g |` D ) = ( g |` E ) )
32 30 31 eqeq12d 
 |-  ( f = h -> ( ( f |` D ) = ( g |` D ) <-> ( h |` E ) = ( g |` E ) ) )
33 32 ralbidv 
 |-  ( f = h -> ( A. g e. A ( f |` D ) = ( g |` D ) <-> A. g e. A ( h |` E ) = ( g |` E ) ) )
34 13 33 imbi12d 
 |-  ( f = h -> ( ( f e. A -> A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( h e. A -> A. g e. A ( h |` E ) = ( g |` E ) ) ) )
35 21 24 34 cbvalv1 
 |-  ( A. f ( f e. A -> A. g e. A ( f |` D ) = ( g |` D ) ) <-> A. h ( h e. A -> A. g e. A ( h |` E ) = ( g |` E ) ) )
36 df-ral 
 |-  ( A. f e. A A. g e. A ( f |` D ) = ( g |` D ) <-> A. f ( f e. A -> A. g e. A ( f |` D ) = ( g |` D ) ) )
37 df-ral 
 |-  ( A. h e. A A. g e. A ( h |` E ) = ( g |` E ) <-> A. h ( h e. A -> A. g e. A ( h |` E ) = ( g |` E ) ) )
38 35 36 37 3bitr4i 
 |-  ( A. f e. A A. g e. A ( f |` D ) = ( g |` D ) <-> A. h e. A A. g e. A ( h |` E ) = ( g |` E ) )
39 20 38 anbi12i 
 |-  ( ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) )
40 39 3 7 3bitr4i 
 |-  ( ps <-> ps' )
41 5 6 7 bnj1383 
 |-  ( ps' -> Fun U. A )
42 40 41 sylbi 
 |-  ( ps -> Fun U. A )