ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cc2lem Unicode version

Theorem cc2lem 7086
Description: Lemma for cc2 7087. (Contributed by Jim Kingdon, 27-Apr-2024.)
Hypotheses
Ref Expression
cc2.cc  |-  ( ph  -> CCHOICE )
cc2.a  |-  ( ph  ->  F  Fn  om )
cc2.m  |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
cc2lem.a  |-  A  =  ( n  e.  om  |->  ( { n }  X.  ( F `  n ) ) )
cc2lem.g  |-  G  =  ( n  e.  om  |->  ( 2nd `  ( f `
 ( A `  n ) ) ) )
Assertion
Ref Expression
cc2lem  |-  ( ph  ->  E. g ( g  Fn  om  /\  A. n  e.  om  (
g `  n )  e.  ( F `  n
) ) )
Distinct variable groups:    A, f, n   
w, A, n    n, F, w    f, F, g, n    x, F, n, w    g, G, n    ph, n, w    ph, f
Allowed substitution hints:    ph( x, g)    A( x, g)    G( x, w, f)

Proof of Theorem cc2lem
Dummy variables  z  k  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cc2.cc . . 3  |-  ( ph  -> CCHOICE )
2 vex 2689 . . . . . . . 8  |-  n  e. 
_V
32snex 4109 . . . . . . 7  |-  { n }  e.  _V
4 cc2.a . . . . . . . 8  |-  ( ph  ->  F  Fn  om )
5 funfvex 5438 . . . . . . . . 9  |-  ( ( Fun  F  /\  n  e.  dom  F )  -> 
( F `  n
)  e.  _V )
65funfni 5223 . . . . . . . 8  |-  ( ( F  Fn  om  /\  n  e.  om )  ->  ( F `  n
)  e.  _V )
74, 6sylan 281 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  ( F `  n )  e.  _V )
8 xpexg 4653 . . . . . . 7  |-  ( ( { n }  e.  _V  /\  ( F `  n )  e.  _V )  ->  ( { n }  X.  ( F `  n ) )  e. 
_V )
93, 7, 8sylancr 410 . . . . . 6  |-  ( (
ph  /\  n  e.  om )  ->  ( {
n }  X.  ( F `  n )
)  e.  _V )
10 cc2lem.a . . . . . 6  |-  A  =  ( n  e.  om  |->  ( { n }  X.  ( F `  n ) ) )
119, 10fmptd 5574 . . . . 5  |-  ( ph  ->  A : om --> _V )
12 sneq 3538 . . . . . . . . . 10  |-  ( n  =  k  ->  { n }  =  { k } )
13 fveq2 5421 . . . . . . . . . 10  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
1412, 13xpeq12d 4564 . . . . . . . . 9  |-  ( n  =  k  ->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
) )
15 simprr 521 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
k  e.  om )
16 vex 2689 . . . . . . . . . . 11  |-  k  e. 
_V
1716snex 4109 . . . . . . . . . 10  |-  { k }  e.  _V
184adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  F  Fn  om )
19 funfvex 5438 . . . . . . . . . . . 12  |-  ( ( Fun  F  /\  k  e.  dom  F )  -> 
( F `  k
)  e.  _V )
2019funfni 5223 . . . . . . . . . . 11  |-  ( ( F  Fn  om  /\  k  e.  om )  ->  ( F `  k
)  e.  _V )
2118, 15, 20syl2anc 408 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( F `  k
)  e.  _V )
22 xpexg 4653 . . . . . . . . . 10  |-  ( ( { k }  e.  _V  /\  ( F `  k )  e.  _V )  ->  ( { k }  X.  ( F `
 k ) )  e.  _V )
2317, 21, 22sylancr 410 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( { k }  X.  ( F `  k ) )  e. 
_V )
2410, 14, 15, 23fvmptd3 5514 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( A `  k
)  =  ( { k }  X.  ( F `  k )
) )
2524eqeq2d 2151 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( A `  k )  <-> 
( A `  n
)  =  ( { k }  X.  ( F `  k )
) ) )
26 simpr 109 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  om )  ->  n  e.  om )
2710fvmpt2 5504 . . . . . . . . . . 11  |-  ( ( n  e.  om  /\  ( { n }  X.  ( F `  n ) )  e.  _V )  ->  ( A `  n
)  =  ( { n }  X.  ( F `  n )
) )
2826, 9, 27syl2anc 408 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  =  ( { n }  X.  ( F `  n ) ) )
2928adantrr 470 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( A `  n
)  =  ( { n }  X.  ( F `  n )
) )
3029eqeq1d 2148 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( { k }  X.  ( F `  k ) )  <->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) ) ) )
312snm 3643 . . . . . . . . . 10  |-  E. w  w  e.  { n }
32 fveq2 5421 . . . . . . . . . . . . 13  |-  ( x  =  n  ->  ( F `  x )  =  ( F `  n ) )
3332eleq2d 2209 . . . . . . . . . . . 12  |-  ( x  =  n  ->  (
w  e.  ( F `
 x )  <->  w  e.  ( F `  n ) ) )
3433exbidv 1797 . . . . . . . . . . 11  |-  ( x  =  n  ->  ( E. w  w  e.  ( F `  x )  <->  E. w  w  e.  ( F `  n ) ) )
35 cc2.m . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
3635adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
37 simprl 520 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  n  e.  om )
3834, 36, 37rspcdva 2794 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  E. w  w  e.  ( F `  n ) )
39 xp11m 4977 . . . . . . . . . 10  |-  ( ( E. w  w  e. 
{ n }  /\  E. w  w  e.  ( F `  n ) )  ->  ( ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
)  <->  ( { n }  =  { k }  /\  ( F `  n )  =  ( F `  k ) ) ) )
4031, 38, 39sylancr 410 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) )  <->  ( {
n }  =  {
k }  /\  ( F `  n )  =  ( F `  k ) ) ) )
412sneqr 3687 . . . . . . . . . 10  |-  ( { n }  =  {
k }  ->  n  =  k )
4241adantr 274 . . . . . . . . 9  |-  ( ( { n }  =  { k }  /\  ( F `  n )  =  ( F `  k ) )  ->  n  =  k )
4340, 42syl6bi 162 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) )  ->  n  =  k )
)
4430, 43sylbid 149 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( { k }  X.  ( F `  k ) )  ->  n  =  k ) )
4525, 44sylbid 149 . . . . . 6  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( A `  k )  ->  n  =  k ) )
4645ralrimivva 2514 . . . . 5  |-  ( ph  ->  A. n  e.  om  A. k  e.  om  (
( A `  n
)  =  ( A `
 k )  ->  n  =  k )
)
47 dff13 5669 . . . . 5  |-  ( A : om -1-1-> _V  <->  ( A : om --> _V  /\  A. n  e.  om  A. k  e. 
om  ( ( A `
 n )  =  ( A `  k
)  ->  n  =  k ) ) )
4811, 46, 47sylanbrc 413 . . . 4  |-  ( ph  ->  A : om -1-1-> _V )
49 f1f1orn 5378 . . . . 5  |-  ( A : om -1-1-> _V  ->  A : om -1-1-onto-> ran  A )
50 omex 4507 . . . . . 6  |-  om  e.  _V
5150f1oen 6653 . . . . 5  |-  ( A : om -1-1-onto-> ran  A  ->  om  ~~  ran  A )
52 ensym 6675 . . . . 5  |-  ( om 
~~  ran  A  ->  ran 
A  ~~  om )
5349, 51, 523syl 17 . . . 4  |-  ( A : om -1-1-> _V  ->  ran 
A  ~~  om )
5448, 53syl 14 . . 3  |-  ( ph  ->  ran  A  ~~  om )
559ralrimiva 2505 . . . . . . . . 9  |-  ( ph  ->  A. n  e.  om  ( { n }  X.  ( F `  n ) )  e.  _V )
5610fnmpt 5249 . . . . . . . . 9  |-  ( A. n  e.  om  ( { n }  X.  ( F `  n ) )  e.  _V  ->  A  Fn  om )
5755, 56syl 14 . . . . . . . 8  |-  ( ph  ->  A  Fn  om )
5857adantr 274 . . . . . . 7  |-  ( (
ph  /\  z  e.  ran  A )  ->  A  Fn  om )
59 fnfun 5220 . . . . . . 7  |-  ( A  Fn  om  ->  Fun  A )
6058, 59syl 14 . . . . . 6  |-  ( (
ph  /\  z  e.  ran  A )  ->  Fun  A )
61 simpr 109 . . . . . 6  |-  ( (
ph  /\  z  e.  ran  A )  ->  z  e.  ran  A )
62 elrnrexdm 5559 . . . . . 6  |-  ( Fun 
A  ->  ( z  e.  ran  A  ->  E. n  e.  dom  A  z  =  ( A `  n
) ) )
6360, 61, 62sylc 62 . . . . 5  |-  ( (
ph  /\  z  e.  ran  A )  ->  E. n  e.  dom  A  z  =  ( A `  n
) )
64 simpll 518 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  ph )
65 simprl 520 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  n  e.  dom  A )
66 fndm 5222 . . . . . . . . 9  |-  ( A  Fn  om  ->  dom  A  =  om )
6764, 57, 663syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  dom  A  =  om )
6865, 67eleqtrd 2218 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  n  e.  om )
6935adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  om )  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
7034, 69, 26rspcdva 2794 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( F `  n ) )
71 eleq1 2202 . . . . . . . . . . 11  |-  ( w  =  a  ->  (
w  e.  ( F `
 n )  <->  a  e.  ( F `  n ) ) )
7271cbvexv 1890 . . . . . . . . . 10  |-  ( E. w  w  e.  ( F `  n )  <->  E. a  a  e.  ( F `  n ) )
7370, 72sylib 121 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  E. a 
a  e.  ( F `
 n ) )
74 vsnid 3557 . . . . . . . . . . 11  |-  n  e. 
{ n }
75 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  a  e.  ( F `  n
) )  ->  a  e.  ( F `  n
) )
76 opelxpi 4571 . . . . . . . . . . 11  |-  ( ( n  e.  { n }  /\  a  e.  ( F `  n ) )  ->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) )
7774, 75, 76sylancr 410 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  om )  /\  a  e.  ( F `  n
) )  ->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) )
78 eleq1 2202 . . . . . . . . . . 11  |-  ( w  =  <. n ,  a
>.  ->  ( w  e.  ( { n }  X.  ( F `  n
) )  <->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) ) )
7978spcegv 2774 . . . . . . . . . 10  |-  ( <.
n ,  a >.  e.  ( { n }  X.  ( F `  n
) )  ->  ( <. n ,  a >.  e.  ( { n }  X.  ( F `  n
) )  ->  E. w  w  e.  ( {
n }  X.  ( F `  n )
) ) )
8077, 77, 79sylc 62 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  om )  /\  a  e.  ( F `  n
) )  ->  E. w  w  e.  ( {
n }  X.  ( F `  n )
) )
8173, 80exlimddv 1870 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( {
n }  X.  ( F `  n )
) )
8228eleq2d 2209 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  ( w  e.  ( A `  n
)  <->  w  e.  ( { n }  X.  ( F `  n ) ) ) )
8382exbidv 1797 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  ( E. w  w  e.  ( A `  n )  <->  E. w  w  e.  ( { n }  X.  ( F `  n ) ) ) )
8481, 83mpbird 166 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( A `  n ) )
8564, 68, 84syl2anc 408 . . . . . 6  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  E. w  w  e.  ( A `  n ) )
86 simprr 521 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  z  =  ( A `  n ) )
8786eleq2d 2209 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  (
w  e.  z  <->  w  e.  ( A `  n ) ) )
8887exbidv 1797 . . . . . 6  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  ( E. w  w  e.  z 
<->  E. w  w  e.  ( A `  n
) ) )
8985, 88mpbird 166 . . . . 5  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  E. w  w  e.  z )
9063, 89rexlimddv 2554 . . . 4  |-  ( (
ph  /\  z  e.  ran  A )  ->  E. w  w  e.  z )
9190ralrimiva 2505 . . 3  |-  ( ph  ->  A. z  e.  ran  A E. w  w  e.  z )
921, 54, 91ccfunen 7084 . 2  |-  ( ph  ->  E. f ( f  Fn  ran  A  /\  A. z  e.  ran  A
( f `  z
)  e.  z ) )
93 vex 2689 . . . . . . . 8  |-  f  e. 
_V
94 funfvex 5438 . . . . . . . . . 10  |-  ( ( Fun  A  /\  n  e.  dom  A )  -> 
( A `  n
)  e.  _V )
9594funfni 5223 . . . . . . . . 9  |-  ( ( A  Fn  om  /\  n  e.  om )  ->  ( A `  n
)  e.  _V )
9657, 95sylan 281 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  e.  _V )
97 fvexg 5440 . . . . . . . 8  |-  ( ( f  e.  _V  /\  ( A `  n )  e.  _V )  -> 
( f `  ( A `  n )
)  e.  _V )
9893, 96, 97sylancr 410 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  ( f `  ( A `  n
) )  e.  _V )
99 2ndexg 6066 . . . . . . 7  |-  ( ( f `  ( A `
 n ) )  e.  _V  ->  ( 2nd `  ( f `  ( A `  n ) ) )  e.  _V )
10098, 99syl 14 . . . . . 6  |-  ( (
ph  /\  n  e.  om )  ->  ( 2nd `  ( f `  ( A `  n )
) )  e.  _V )
101100ralrimiva 2505 . . . . 5  |-  ( ph  ->  A. n  e.  om  ( 2nd `  ( f `
 ( A `  n ) ) )  e.  _V )
102 cc2lem.g . . . . . 6  |-  G  =  ( n  e.  om  |->  ( 2nd `  ( f `
 ( A `  n ) ) ) )
103102fnmpt 5249 . . . . 5  |-  ( A. n  e.  om  ( 2nd `  ( f `  ( A `  n ) ) )  e.  _V  ->  G  Fn  om )
104101, 103syl 14 . . . 4  |-  ( ph  ->  G  Fn  om )
105104adantr 274 . . 3  |-  ( (
ph  /\  ( f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z )  e.  z ) )  ->  G  Fn  om )
106 simpr 109 . . . . . 6  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  n  e.  om )
107 fveq2 5421 . . . . . . . . . 10  |-  ( z  =  ( A `  n )  ->  (
f `  z )  =  ( f `  ( A `  n ) ) )
108 id 19 . . . . . . . . . 10  |-  ( z  =  ( A `  n )  ->  z  =  ( A `  n ) )
109107, 108eleq12d 2210 . . . . . . . . 9  |-  ( z  =  ( A `  n )  ->  (
( f `  z
)  e.  z  <->  ( f `  ( A `  n
) )  e.  ( A `  n ) ) )
110 simplrr 525 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  A. z  e.  ran  A ( f `
 z )  e.  z )
111 fnfvelrn 5552 . . . . . . . . . . 11  |-  ( ( A  Fn  om  /\  n  e.  om )  ->  ( A `  n
)  e.  ran  A
)
11257, 111sylan 281 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  e.  ran  A )
113112adantlr 468 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  ( A `  n )  e.  ran  A )
114109, 110, 113rspcdva 2794 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  (
f `  ( A `  n ) )  e.  ( A `  n
) )
11528eleq2d 2209 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  ( (
f `  ( A `  n ) )  e.  ( A `  n
)  <->  ( f `  ( A `  n ) )  e.  ( { n }  X.  ( F `  n )
) ) )
116115adantlr 468 . . . . . . . 8  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  (
( f `  ( A `  n )
)  e.  ( A `
 n )  <->  ( f `  ( A `  n
) )  e.  ( { n }  X.  ( F `  n ) ) ) )
117114, 116mpbid 146 . . . . . . 7  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  (
f `  ( A `  n ) )  e.  ( { n }  X.  ( F `  n
) ) )
118 xp2nd 6064 . . . . . . 7  |-  ( ( f `  ( A `
 n ) )  e.  ( { n }  X.  ( F `  n ) )  -> 
( 2nd `  (
f `  ( A `  n ) ) )  e.  ( F `  n ) )
119117, 118syl 14 . . . . . 6  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  ( 2nd `  ( f `  ( A `  n ) ) )  e.  ( F `  n ) )
120102fvmpt2 5504 . . . . . 6  |-  ( ( n  e.  om  /\  ( 2nd `  ( f `
 ( A `  n ) ) )  e.  ( F `  n ) )  -> 
( G `  n
)  =  ( 2nd `  ( f `  ( A `  n )
) ) )
121106, 119, 120syl2anc 408 . . . . 5  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  ( G `  n )  =  ( 2nd `  (
f `  ( A `  n ) ) ) )
122121, 119eqeltrd 2216 . . . 4  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  ( G `  n )  e.  ( F `  n
) )
123122ralrimiva 2505 . . 3  |-  ( (
ph  /\  ( f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z )  e.  z ) )  ->  A. n  e.  om  ( G `  n )  e.  ( F `  n ) )
12450a1i 9 . . . . . 6  |-  ( ph  ->  om  e.  _V )
125 fnex 5642 . . . . . 6  |-  ( ( G  Fn  om  /\  om  e.  _V )  ->  G  e.  _V )
126104, 124, 125syl2anc 408 . . . . 5  |-  ( ph  ->  G  e.  _V )
127 fneq1 5211 . . . . . . 7  |-  ( g  =  G  ->  (
g  Fn  om  <->  G  Fn  om ) )
128 fveq1 5420 . . . . . . . . 9  |-  ( g  =  G  ->  (
g `  n )  =  ( G `  n ) )
129128eleq1d 2208 . . . . . . . 8  |-  ( g  =  G  ->  (
( g `  n
)  e.  ( F `
 n )  <->  ( G `  n )  e.  ( F `  n ) ) )
130129ralbidv 2437 . . . . . . 7  |-  ( g  =  G  ->  ( A. n  e.  om  ( g `  n
)  e.  ( F `
 n )  <->  A. n  e.  om  ( G `  n )  e.  ( F `  n ) ) )
131127, 130anbi12d 464 . . . . . 6  |-  ( g  =  G  ->  (
( g  Fn  om  /\ 
A. n  e.  om  ( g `  n
)  e.  ( F `
 n ) )  <-> 
( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ( F `  n ) ) ) )
132131spcegv 2774 . . . . 5  |-  ( G  e.  _V  ->  (
( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ( F `  n ) )  ->  E. g ( g  Fn 
om  /\  A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) ) )
133126, 132syl 14 . . . 4  |-  ( ph  ->  ( ( G  Fn  om 
/\  A. n  e.  om  ( G `  n )  e.  ( F `  n ) )  ->  E. g ( g  Fn 
om  /\  A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) ) )
134133adantr 274 . . 3  |-  ( (
ph  /\  ( f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z )  e.  z ) )  ->  ( ( G  Fn  om  /\  A. n  e.  om  ( G `  n )  e.  ( F `  n
) )  ->  E. g
( g  Fn  om  /\ 
A. n  e.  om  ( g `  n
)  e.  ( F `
 n ) ) ) )
135105, 123, 134mp2and 429 . 2  |-  ( (
ph  /\  ( f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z )  e.  z ) )  ->  E. g ( g  Fn  om  /\  A. n  e.  om  (
g `  n )  e.  ( F `  n
) ) )
13692, 135exlimddv 1870 1  |-  ( ph  ->  E. g ( g  Fn  om  /\  A. n  e.  om  (
g `  n )  e.  ( F `  n
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1331   E.wex 1468    e. wcel 1480   A.wral 2416   E.wrex 2417   _Vcvv 2686   {csn 3527   <.cop 3530   class class class wbr 3929    |-> cmpt 3989   omcom 4504    X. cxp 4537   dom cdm 4539   ran crn 4540   Fun wfun 5117    Fn wfn 5118   -->wf 5119   -1-1->wf1 5120   -1-1-onto->wf1o 5122   ` cfv 5123   2ndc2nd 6037    ~~ cen 6632  CCHOICEwacc 7082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-2nd 6039  df-er 6429  df-en 6635  df-cc 7083
This theorem is referenced by:  cc2  7087
  Copyright terms: Public domain W3C validator