Metamath Proof Explorer

Theorem imasvscafn

Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasvscaf.u 
|- ( ph -> U = ( F "s R ) )
imasvscaf.v 
|- ( ph -> V = ( Base ` R ) )
imasvscaf.f 
|- ( ph -> F : V -onto-> B )
imasvscaf.r 
|- ( ph -> R e. Z )
imasvscaf.g 
|- G = ( Scalar ` R )
imasvscaf.k 
|- K = ( Base ` G )
imasvscaf.q 
|- .x. = ( .s ` R )
imasvscaf.s 
|- .xb = ( .s ` U )
imasvscaf.e 
|- ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
Assertion imasvscafn 
|- ( ph -> .xb Fn ( K X. B ) )

Proof

Step Hyp Ref Expression
1 imasvscaf.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasvscaf.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasvscaf.f 
 |-  ( ph -> F : V -onto-> B )
4 imasvscaf.r 
 |-  ( ph -> R e. Z )
5 imasvscaf.g 
 |-  G = ( Scalar ` R )
6 imasvscaf.k 
 |-  K = ( Base ` G )
7 imasvscaf.q 
 |-  .x. = ( .s ` R )
8 imasvscaf.s 
 |-  .xb = ( .s ` U )
9 imasvscaf.e 
 |-  ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
10 eqid 
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
11 fvex 
 |-  ( F ` ( p .x. q ) ) e. _V
12 10 11 fnmpoi 
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } )
13 fnrel 
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } ) -> Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
14 12 13 ax-mp 
 |-  Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
15 14 rgenw 
 |-  A. q e. V Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
16 reliun 
 |-  ( Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) <-> A. q e. V Rel ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
17 15 16 mpbir 
 |-  Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
18 1 2 3 4 5 6 7 8 imasvsca 
 |-  ( ph -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
19 18 releqd 
 |-  ( ph -> ( Rel .xb <-> Rel U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
20 17 19 mpbiri 
 |-  ( ph -> Rel .xb )
21 dffn2 
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) Fn ( K X. { ( F ` q ) } ) <-> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V )
22 12 21 mpbi 
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V
23 fssxp 
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) : ( K X. { ( F ` q ) } ) --> _V -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. _V ) )
24 22 23 ax-mp 
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. { ( F ` q ) } ) X. _V )
25 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
26 3 25 syl 
 |-  ( ph -> F : V --> B )
27 26 ffvelrnda 
 |-  ( ( ph /\ q e. V ) -> ( F ` q ) e. B )
28 27 snssd 
 |-  ( ( ph /\ q e. V ) -> { ( F ` q ) } C_ B )
29 xpss2 
 |-  ( { ( F ` q ) } C_ B -> ( K X. { ( F ` q ) } ) C_ ( K X. B ) )
30 xpss1 
 |-  ( ( K X. { ( F ` q ) } ) C_ ( K X. B ) -> ( ( K X. { ( F ` q ) } ) X. _V ) C_ ( ( K X. B ) X. _V ) )
31 28 29 30 3syl 
 |-  ( ( ph /\ q e. V ) -> ( ( K X. { ( F ` q ) } ) X. _V ) C_ ( ( K X. B ) X. _V ) )
32 24 31 sstrid 
 |-  ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
33 32 ralrimiva 
 |-  ( ph -> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
34 iunss 
 |-  ( U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) <-> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
35 33 34 sylibr 
 |-  ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ ( ( K X. B ) X. _V ) )
36 18 35 eqsstrd 
 |-  ( ph -> .xb C_ ( ( K X. B ) X. _V ) )
37 dmss 
 |-  ( .xb C_ ( ( K X. B ) X. _V ) -> dom .xb C_ dom ( ( K X. B ) X. _V ) )
38 36 37 syl 
 |-  ( ph -> dom .xb C_ dom ( ( K X. B ) X. _V ) )
39 vn0 
 |-  _V =/= (/)
40 dmxp 
 |-  ( _V =/= (/) -> dom ( ( K X. B ) X. _V ) = ( K X. B ) )
41 39 40 ax-mp 
 |-  dom ( ( K X. B ) X. _V ) = ( K X. B )
42 38 41 sseqtrdi 
 |-  ( ph -> dom .xb C_ ( K X. B ) )
43 forn 
 |-  ( F : V -onto-> B -> ran F = B )
44 3 43 syl 
 |-  ( ph -> ran F = B )
45 44 xpeq2d 
 |-  ( ph -> ( K X. ran F ) = ( K X. B ) )
46 42 45 sseqtrrd 
 |-  ( ph -> dom .xb C_ ( K X. ran F ) )
47 df-br 
 |-  ( <. p , ( F ` a ) >. .xb w <-> <. <. p , ( F ` a ) >. , w >. e. .xb )
48 18 eleq2d 
 |-  ( ph -> ( <. <. p , ( F ` a ) >. , w >. e. .xb <-> <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. .xb <-> <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) )
50 eliun 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) <-> E. q e. V <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
51 df-3an 
 |-  ( ( p e. K /\ a e. V /\ q e. V ) <-> ( ( p e. K /\ a e. V ) /\ q e. V ) )
52 10 mpofun 
 |-  Fun ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) )
53 funopfv 
 |-  ( Fun ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = w ) )
54 52 53 ax-mp 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = w )
55 df-ov 
 |-  ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. )
56 opex 
 |-  <. p , ( F ` a ) >. e. _V
57 vex 
 |-  w e. _V
58 56 57 opeldm 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> <. p , ( F ` a ) >. e. dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
59 10 11 dmmpo 
 |-  dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( K X. { ( F ` q ) } )
60 58 59 eleqtrdi 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> <. p , ( F ` a ) >. e. ( K X. { ( F ` q ) } ) )
61 opelxp 
 |-  ( <. p , ( F ` a ) >. e. ( K X. { ( F ` q ) } ) <-> ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) )
62 60 61 sylib 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) )
63 fvoveq1 
 |-  ( z = p -> ( F ` ( z .x. q ) ) = ( F ` ( p .x. q ) ) )
64 eqidd 
 |-  ( y = ( F ` a ) -> ( F ` ( p .x. q ) ) = ( F ` ( p .x. q ) ) )
65 fvoveq1 
 |-  ( p = z -> ( F ` ( p .x. q ) ) = ( F ` ( z .x. q ) ) )
66 eqidd 
 |-  ( x = y -> ( F ` ( z .x. q ) ) = ( F ` ( z .x. q ) ) )
67 65 66 cbvmpov 
 |-  ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = ( z e. K , y e. { ( F ` q ) } |-> ( F ` ( z .x. q ) ) )
68 63 64 67 11 ovmpo 
 |-  ( ( p e. K /\ ( F ` a ) e. { ( F ` q ) } ) -> ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( F ` ( p .x. q ) ) )
69 62 68 syl 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( p ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ( F ` a ) ) = ( F ` ( p .x. q ) ) )
70 55 69 eqtr3id 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ` <. p , ( F ` a ) >. ) = ( F ` ( p .x. q ) ) )
71 54 70 eqtr3d 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. q ) ) )
72 71 adantl 
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> w = ( F ` ( p .x. q ) ) )
73 elsni 
 |-  ( ( F ` a ) e. { ( F ` q ) } -> ( F ` a ) = ( F ` q ) )
74 62 73 simpl2im 
 |-  ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> ( F ` a ) = ( F ` q ) )
75 9 74 impel 
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) )
76 72 75 eqtr4d 
 |-  ( ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) /\ <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) -> w = ( F ` ( p .x. a ) ) )
77 76 ex 
 |-  ( ( ph /\ ( p e. K /\ a e. V /\ q e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
78 51 77 sylan2br 
 |-  ( ( ph /\ ( ( p e. K /\ a e. V ) /\ q e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
79 78 anassrs 
 |-  ( ( ( ph /\ ( p e. K /\ a e. V ) ) /\ q e. V ) -> ( <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
80 79 rexlimdva 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( E. q e. V <. <. p , ( F ` a ) >. , w >. e. ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
81 50 80 syl5bi 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> w = ( F ` ( p .x. a ) ) ) )
82 49 81 sylbid 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. <. p , ( F ` a ) >. , w >. e. .xb -> w = ( F ` ( p .x. a ) ) ) )
83 47 82 syl5bi 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) )
84 83 alrimiv 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> A. w ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) )
85 mo2icl 
 |-  ( A. w ( <. p , ( F ` a ) >. .xb w -> w = ( F ` ( p .x. a ) ) ) -> E* w <. p , ( F ` a ) >. .xb w )
86 84 85 syl 
 |-  ( ( ph /\ ( p e. K /\ a e. V ) ) -> E* w <. p , ( F ` a ) >. .xb w )
87 86 ralrimivva 
 |-  ( ph -> A. p e. K A. a e. V E* w <. p , ( F ` a ) >. .xb w )
88 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
89 opeq2 
 |-  ( y = ( F ` a ) -> <. p , y >. = <. p , ( F ` a ) >. )
90 89 breq1d 
 |-  ( y = ( F ` a ) -> ( <. p , y >. .xb w <-> <. p , ( F ` a ) >. .xb w ) )
91 90 mobidv 
 |-  ( y = ( F ` a ) -> ( E* w <. p , y >. .xb w <-> E* w <. p , ( F ` a ) >. .xb w ) )
92 91 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F E* w <. p , y >. .xb w <-> A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
93 3 88 92 3syl 
 |-  ( ph -> ( A. y e. ran F E* w <. p , y >. .xb w <-> A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
94 93 ralbidv 
 |-  ( ph -> ( A. p e. K A. y e. ran F E* w <. p , y >. .xb w <-> A. p e. K A. a e. V E* w <. p , ( F ` a ) >. .xb w ) )
95 87 94 mpbird 
 |-  ( ph -> A. p e. K A. y e. ran F E* w <. p , y >. .xb w )
96 breq1 
 |-  ( x = <. p , y >. -> ( x .xb w <-> <. p , y >. .xb w ) )
97 96 mobidv 
 |-  ( x = <. p , y >. -> ( E* w x .xb w <-> E* w <. p , y >. .xb w ) )
98 97 ralxp 
 |-  ( A. x e. ( K X. ran F ) E* w x .xb w <-> A. p e. K A. y e. ran F E* w <. p , y >. .xb w )
99 95 98 sylibr 
 |-  ( ph -> A. x e. ( K X. ran F ) E* w x .xb w )
100 ssralv 
 |-  ( dom .xb C_ ( K X. ran F ) -> ( A. x e. ( K X. ran F ) E* w x .xb w -> A. x e. dom .xb E* w x .xb w ) )
101 46 99 100 sylc 
 |-  ( ph -> A. x e. dom .xb E* w x .xb w )
102 dffun7 
 |-  ( Fun .xb <-> ( Rel .xb /\ A. x e. dom .xb E* w x .xb w ) )
103 20 101 102 sylanbrc 
 |-  ( ph -> Fun .xb )
104 eqimss2 
 |-  ( .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
105 18 104 syl 
 |-  ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
106 iunss 
 |-  ( U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb <-> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
107 105 106 sylib 
 |-  ( ph -> A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
108 107 r19.21bi 
 |-  ( ( ph /\ q e. V ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
109 108 adantrl 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb )
110 dmss 
 |-  ( ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ .xb -> dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ dom .xb )
111 109 110 syl 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> dom ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) C_ dom .xb )
112 59 111 eqsstrrid 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> ( K X. { ( F ` q ) } ) C_ dom .xb )
113 simprl 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> p e. K )
114 fvex 
 |-  ( F ` q ) e. _V
115 114 snid 
 |-  ( F ` q ) e. { ( F ` q ) }
116 opelxpi 
 |-  ( ( p e. K /\ ( F ` q ) e. { ( F ` q ) } ) -> <. p , ( F ` q ) >. e. ( K X. { ( F ` q ) } ) )
117 113 115 116 sylancl 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> <. p , ( F ` q ) >. e. ( K X. { ( F ` q ) } ) )
118 112 117 sseldd 
 |-  ( ( ph /\ ( p e. K /\ q e. V ) ) -> <. p , ( F ` q ) >. e. dom .xb )
119 118 ralrimivva 
 |-  ( ph -> A. p e. K A. q e. V <. p , ( F ` q ) >. e. dom .xb )
120 opeq2 
 |-  ( y = ( F ` q ) -> <. p , y >. = <. p , ( F ` q ) >. )
121 120 eleq1d 
 |-  ( y = ( F ` q ) -> ( <. p , y >. e. dom .xb <-> <. p , ( F ` q ) >. e. dom .xb ) )
122 121 ralrn 
 |-  ( F Fn V -> ( A. y e. ran F <. p , y >. e. dom .xb <-> A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
123 3 88 122 3syl 
 |-  ( ph -> ( A. y e. ran F <. p , y >. e. dom .xb <-> A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
124 123 ralbidv 
 |-  ( ph -> ( A. p e. K A. y e. ran F <. p , y >. e. dom .xb <-> A. p e. K A. q e. V <. p , ( F ` q ) >. e. dom .xb ) )
125 119 124 mpbird 
 |-  ( ph -> A. p e. K A. y e. ran F <. p , y >. e. dom .xb )
126 eleq1 
 |-  ( x = <. p , y >. -> ( x e. dom .xb <-> <. p , y >. e. dom .xb ) )
127 126 ralxp 
 |-  ( A. x e. ( K X. ran F ) x e. dom .xb <-> A. p e. K A. y e. ran F <. p , y >. e. dom .xb )
128 125 127 sylibr 
 |-  ( ph -> A. x e. ( K X. ran F ) x e. dom .xb )
129 dfss3 
 |-  ( ( K X. ran F ) C_ dom .xb <-> A. x e. ( K X. ran F ) x e. dom .xb )
130 128 129 sylibr 
 |-  ( ph -> ( K X. ran F ) C_ dom .xb )
131 45 130 eqsstrrd 
 |-  ( ph -> ( K X. B ) C_ dom .xb )
132 42 131 eqssd 
 |-  ( ph -> dom .xb = ( K X. B ) )
133 df-fn 
 |-  ( .xb Fn ( K X. B ) <-> ( Fun .xb /\ dom .xb = ( K X. B ) ) )
134 103 132 133 sylanbrc 
 |-  ( ph -> .xb Fn ( K X. B ) )