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

Theorem cc2lem 7377
Description: Lemma for cc2 7378. (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 2774 . . . . . . . 8  |-  n  e. 
_V
32snex 4228 . . . . . . 7  |-  { n }  e.  _V
4 cc2.a . . . . . . . 8  |-  ( ph  ->  F  Fn  om )
5 funfvex 5592 . . . . . . . . 9  |-  ( ( Fun  F  /\  n  e.  dom  F )  -> 
( F `  n
)  e.  _V )
65funfni 5375 . . . . . . . 8  |-  ( ( F  Fn  om  /\  n  e.  om )  ->  ( F `  n
)  e.  _V )
74, 6sylan 283 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  ( F `  n )  e.  _V )
8 xpexg 4788 . . . . . . 7  |-  ( ( { n }  e.  _V  /\  ( F `  n )  e.  _V )  ->  ( { n }  X.  ( F `  n ) )  e. 
_V )
93, 7, 8sylancr 414 . . . . . 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 5733 . . . . 5  |-  ( ph  ->  A : om --> _V )
12 sneq 3643 . . . . . . . . . 10  |-  ( n  =  k  ->  { n }  =  { k } )
13 fveq2 5575 . . . . . . . . . 10  |-  ( n  =  k  ->  ( F `  n )  =  ( F `  k ) )
1412, 13xpeq12d 4699 . . . . . . . . 9  |-  ( n  =  k  ->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k )
) )
15 simprr 531 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
k  e.  om )
16 vex 2774 . . . . . . . . . . 11  |-  k  e. 
_V
1716snex 4228 . . . . . . . . . 10  |-  { k }  e.  _V
184adantr 276 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  F  Fn  om )
19 funfvex 5592 . . . . . . . . . . . 12  |-  ( ( Fun  F  /\  k  e.  dom  F )  -> 
( F `  k
)  e.  _V )
2019funfni 5375 . . . . . . . . . . 11  |-  ( ( F  Fn  om  /\  k  e.  om )  ->  ( F `  k
)  e.  _V )
2118, 15, 20syl2anc 411 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( F `  k
)  e.  _V )
22 xpexg 4788 . . . . . . . . . 10  |-  ( ( { k }  e.  _V  /\  ( F `  k )  e.  _V )  ->  ( { k }  X.  ( F `
 k ) )  e.  _V )
2317, 21, 22sylancr 414 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( { k }  X.  ( F `  k ) )  e. 
_V )
2410, 14, 15, 23fvmptd3 5672 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( A `  k
)  =  ( { k }  X.  ( F `  k )
) )
2524eqeq2d 2216 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( A `  k )  <-> 
( A `  n
)  =  ( { k }  X.  ( F `  k )
) ) )
26 simpr 110 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  om )  ->  n  e.  om )
2710fvmpt2 5662 . . . . . . . . . . 11  |-  ( ( n  e.  om  /\  ( { n }  X.  ( F `  n ) )  e.  _V )  ->  ( A `  n
)  =  ( { n }  X.  ( F `  n )
) )
2826, 9, 27syl2anc 411 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  =  ( { n }  X.  ( F `  n ) ) )
2928adantrr 479 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( A `  n
)  =  ( { n }  X.  ( F `  n )
) )
3029eqeq1d 2213 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( { k }  X.  ( F `  k ) )  <->  ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) ) ) )
312snm 3752 . . . . . . . . . 10  |-  E. w  w  e.  { n }
32 fveq2 5575 . . . . . . . . . . . . 13  |-  ( x  =  n  ->  ( F `  x )  =  ( F `  n ) )
3332eleq2d 2274 . . . . . . . . . . . 12  |-  ( x  =  n  ->  (
w  e.  ( F `
 x )  <->  w  e.  ( F `  n ) ) )
3433exbidv 1847 . . . . . . . . . . 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 276 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
37 simprl 529 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  n  e.  om )
3834, 36, 37rspcdva 2881 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  ->  E. w  w  e.  ( F `  n ) )
39 xp11m 5120 . . . . . . . . . 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 414 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) )  <->  ( {
n }  =  {
k }  /\  ( F `  n )  =  ( F `  k ) ) ) )
412sneqr 3800 . . . . . . . . . 10  |-  ( { n }  =  {
k }  ->  n  =  k )
4241adantr 276 . . . . . . . . 9  |-  ( ( { n }  =  { k }  /\  ( F `  n )  =  ( F `  k ) )  ->  n  =  k )
4340, 42biimtrdi 163 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( { n }  X.  ( F `  n ) )  =  ( { k }  X.  ( F `  k ) )  ->  n  =  k )
)
4430, 43sylbid 150 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( { k }  X.  ( F `  k ) )  ->  n  =  k ) )
4525, 44sylbid 150 . . . . . 6  |-  ( (
ph  /\  ( n  e.  om  /\  k  e. 
om ) )  -> 
( ( A `  n )  =  ( A `  k )  ->  n  =  k ) )
4645ralrimivva 2587 . . . . 5  |-  ( ph  ->  A. n  e.  om  A. k  e.  om  (
( A `  n
)  =  ( A `
 k )  ->  n  =  k )
)
47 dff13 5836 . . . . 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 417 . . . 4  |-  ( ph  ->  A : om -1-1-> _V )
49 f1f1orn 5532 . . . . 5  |-  ( A : om -1-1-> _V  ->  A : om -1-1-onto-> ran  A )
50 omex 4640 . . . . . 6  |-  om  e.  _V
5150f1oen 6849 . . . . 5  |-  ( A : om -1-1-onto-> ran  A  ->  om  ~~  ran  A )
52 ensym 6872 . . . . 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 2578 . . . . . . . . 9  |-  ( ph  ->  A. n  e.  om  ( { n }  X.  ( F `  n ) )  e.  _V )
5610fnmpt 5401 . . . . . . . . 9  |-  ( A. n  e.  om  ( { n }  X.  ( F `  n ) )  e.  _V  ->  A  Fn  om )
5755, 56syl 14 . . . . . . . 8  |-  ( ph  ->  A  Fn  om )
5857adantr 276 . . . . . . 7  |-  ( (
ph  /\  z  e.  ran  A )  ->  A  Fn  om )
59 fnfun 5370 . . . . . . 7  |-  ( A  Fn  om  ->  Fun  A )
6058, 59syl 14 . . . . . 6  |-  ( (
ph  /\  z  e.  ran  A )  ->  Fun  A )
61 simpr 110 . . . . . 6  |-  ( (
ph  /\  z  e.  ran  A )  ->  z  e.  ran  A )
62 elrnrexdm 5718 . . . . . 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 527 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  ph )
65 simprl 529 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  n  e.  dom  A )
66 fndm 5372 . . . . . . . . 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 2283 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  n  e.  om )
6935adantr 276 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  om )  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )
7034, 69, 26rspcdva 2881 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( F `  n ) )
71 eleq1 2267 . . . . . . . . . . 11  |-  ( w  =  a  ->  (
w  e.  ( F `
 n )  <->  a  e.  ( F `  n ) ) )
7271cbvexv 1941 . . . . . . . . . 10  |-  ( E. w  w  e.  ( F `  n )  <->  E. a  a  e.  ( F `  n ) )
7370, 72sylib 122 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  E. a 
a  e.  ( F `
 n ) )
74 vsnid 3664 . . . . . . . . . . 11  |-  n  e. 
{ n }
75 simpr 110 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  om )  /\  a  e.  ( F `  n
) )  ->  a  e.  ( F `  n
) )
76 opelxpi 4706 . . . . . . . . . . 11  |-  ( ( n  e.  { n }  /\  a  e.  ( F `  n ) )  ->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) )
7774, 75, 76sylancr 414 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  om )  /\  a  e.  ( F `  n
) )  ->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) )
78 eleq1 2267 . . . . . . . . . . 11  |-  ( w  =  <. n ,  a
>.  ->  ( w  e.  ( { n }  X.  ( F `  n
) )  <->  <. n ,  a >.  e.  ( { n }  X.  ( F `  n ) ) ) )
7978spcegv 2860 . . . . . . . . . 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 1921 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( {
n }  X.  ( F `  n )
) )
8228eleq2d 2274 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  ( w  e.  ( A `  n
)  <->  w  e.  ( { n }  X.  ( F `  n ) ) ) )
8382exbidv 1847 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  ( E. w  w  e.  ( A `  n )  <->  E. w  w  e.  ( { n }  X.  ( F `  n ) ) ) )
8481, 83mpbird 167 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  E. w  w  e.  ( A `  n ) )
8564, 68, 84syl2anc 411 . . . . . 6  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  E. w  w  e.  ( A `  n ) )
86 simprr 531 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  z  =  ( A `  n ) )
8786eleq2d 2274 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  (
w  e.  z  <->  w  e.  ( A `  n ) ) )
8887exbidv 1847 . . . . . 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 167 . . . . 5  |-  ( ( ( ph  /\  z  e.  ran  A )  /\  ( n  e.  dom  A  /\  z  =  ( A `  n ) ) )  ->  E. w  w  e.  z )
9063, 89rexlimddv 2627 . . . 4  |-  ( (
ph  /\  z  e.  ran  A )  ->  E. w  w  e.  z )
9190ralrimiva 2578 . . 3  |-  ( ph  ->  A. z  e.  ran  A E. w  w  e.  z )
921, 54, 91ccfunen 7375 . 2  |-  ( ph  ->  E. f ( f  Fn  ran  A  /\  A. z  e.  ran  A
( f `  z
)  e.  z ) )
93 vex 2774 . . . . . . . 8  |-  f  e. 
_V
94 funfvex 5592 . . . . . . . . . 10  |-  ( ( Fun  A  /\  n  e.  dom  A )  -> 
( A `  n
)  e.  _V )
9594funfni 5375 . . . . . . . . 9  |-  ( ( A  Fn  om  /\  n  e.  om )  ->  ( A `  n
)  e.  _V )
9657, 95sylan 283 . . . . . . . 8  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  e.  _V )
97 fvexg 5594 . . . . . . . 8  |-  ( ( f  e.  _V  /\  ( A `  n )  e.  _V )  -> 
( f `  ( A `  n )
)  e.  _V )
9893, 96, 97sylancr 414 . . . . . . 7  |-  ( (
ph  /\  n  e.  om )  ->  ( f `  ( A `  n
) )  e.  _V )
99 2ndexg 6253 . . . . . . 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 2578 . . . . 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 5401 . . . . 5  |-  ( A. n  e.  om  ( 2nd `  ( f `  ( A `  n ) ) )  e.  _V  ->  G  Fn  om )
104101, 103syl 14 . . . 4  |-  ( ph  ->  G  Fn  om )
105104adantr 276 . . 3  |-  ( (
ph  /\  ( f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z )  e.  z ) )  ->  G  Fn  om )
106 simpr 110 . . . . . 6  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  n  e.  om )
107 fveq2 5575 . . . . . . . . . 10  |-  ( z  =  ( A `  n )  ->  (
f `  z )  =  ( f `  ( A `  n ) ) )
108 id 19 . . . . . . . . . 10  |-  ( z  =  ( A `  n )  ->  z  =  ( A `  n ) )
109107, 108eleq12d 2275 . . . . . . . . 9  |-  ( z  =  ( A `  n )  ->  (
( f `  z
)  e.  z  <->  ( f `  ( A `  n
) )  e.  ( A `  n ) ) )
110 simplrr 536 . . . . . . . . 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 5711 . . . . . . . . . . 11  |-  ( ( A  Fn  om  /\  n  e.  om )  ->  ( A `  n
)  e.  ran  A
)
11257, 111sylan 283 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  om )  ->  ( A `  n )  e.  ran  A )
113112adantlr 477 . . . . . . . . 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 2881 . . . . . . . 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 2274 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  om )  ->  ( (
f `  ( A `  n ) )  e.  ( A `  n
)  <->  ( f `  ( A `  n ) )  e.  ( { n }  X.  ( F `  n )
) ) )
116115adantlr 477 . . . . . . . 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 147 . . . . . . 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 6251 . . . . . . 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 5662 . . . . . 6  |-  ( ( n  e.  om  /\  ( 2nd `  ( f `
 ( A `  n ) ) )  e.  ( F `  n ) )  -> 
( G `  n
)  =  ( 2nd `  ( f `  ( A `  n )
) ) )
121106, 119, 120syl2anc 411 . . . . 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 2281 . . . 4  |-  ( ( ( ph  /\  (
f  Fn  ran  A  /\  A. z  e.  ran  A ( f `  z
)  e.  z ) )  /\  n  e. 
om )  ->  ( G `  n )  e.  ( F `  n
) )
123122ralrimiva 2578 . . 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 5805 . . . . . 6  |-  ( ( G  Fn  om  /\  om  e.  _V )  ->  G  e.  _V )
126104, 124, 125syl2anc 411 . . . . 5  |-  ( ph  ->  G  e.  _V )
127 fneq1 5361 . . . . . . 7  |-  ( g  =  G  ->  (
g  Fn  om  <->  G  Fn  om ) )
128 fveq1 5574 . . . . . . . . 9  |-  ( g  =  G  ->  (
g `  n )  =  ( G `  n ) )
129128eleq1d 2273 . . . . . . . 8  |-  ( g  =  G  ->  (
( g `  n
)  e.  ( F `
 n )  <->  ( G `  n )  e.  ( F `  n ) ) )
130129ralbidv 2505 . . . . . . 7  |-  ( g  =  G  ->  ( A. n  e.  om  ( g `  n
)  e.  ( F `
 n )  <->  A. n  e.  om  ( G `  n )  e.  ( F `  n ) ) )
131127, 130anbi12d 473 . . . . . 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 2860 . . . . 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 276 . . 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 433 . 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 1921 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 104    <-> wb 105    = wceq 1372   E.wex 1514    e. wcel 2175   A.wral 2483   E.wrex 2484   _Vcvv 2771   {csn 3632   <.cop 3635   class class class wbr 4043    |-> cmpt 4104   omcom 4637    X. cxp 4672   dom cdm 4674   ran crn 4675   Fun wfun 5264    Fn wfn 5265   -->wf 5266   -1-1->wf1 5267   -1-1-onto->wf1o 5269   ` cfv 5270   2ndc2nd 6224    ~~ cen 6824  CCHOICEwacc 7373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-coll 4158  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-iinf 4635
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-iun 3928  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-iom 4638  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-res 4686  df-ima 4687  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277  df-fv 5278  df-2nd 6226  df-er 6619  df-en 6827  df-cc 7374
This theorem is referenced by:  cc2  7378
  Copyright terms: Public domain W3C validator