Theorem imasaddfnlemg 13261

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)

Hypotheses

Ref	Expression
imasaddf.f	|- ( ph -> F : V -onto-> B )
imasaddf.e	|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
imasaddflem.a	|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
imasaddfnlemg.v	|- ( ph -> V e. W )
imasaddfnlemg.x	|- ( ph -> .x. e. C )

Assertion

Ref	Expression
imasaddfnlemg	|- ( ph -> .xb Fn ( B X. B ) )

Distinct variable groups:   q, p, B   a, b, p, q, V   .x. , p, q   F, a, b, p, q   ph, a, b, p, q   .xb , a, b, p, q

Allowed substitution hints:   B( a, b)   C( q, p, a, b)   .x. ( a, b)   W( q, p, a, b)

Proof of Theorem imasaddfnlemg

Dummy variables w y z x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasaddf.f	. . . . . . . . . . . . 13 |- ( ph -> F : V -onto-> B )
2		fof 5520	. . . . . . . . . . . . 13 |- ( F : V -onto-> B -> F : V --> B )
3	1, 2	syl 14	. . . . . . . . . . . 12 |- ( ph -> F : V --> B )
4		imasaddfnlemg.v	. . . . . . . . . . . 12 |- ( ph -> V e. W )
5	3, 4	fexd 5837	. . . . . . . . . . 11 |- ( ph -> F e. _V )
6		vex 2779	. . . . . . . . . . 11 |- p e. _V
7		fvexg 5618	. . . . . . . . . . 11 |- ( ( F e. _V /\ p e. _V ) -> ( F ` p ) e. _V )
8	5, 6, 7	sylancl 413	. . . . . . . . . 10 |- ( ph -> ( F ` p ) e. _V )
9		vex 2779	. . . . . . . . . . 11 |- q e. _V
10		fvexg 5618	. . . . . . . . . . 11 |- ( ( F e. _V /\ q e. _V ) -> ( F ` q ) e. _V )
11	5, 9, 10	sylancl 413	. . . . . . . . . 10 |- ( ph -> ( F ` q ) e. _V )
12		opexg 4290	. . . . . . . . . 10 |- ( ( ( F ` p ) e. _V /\ ( F ` q ) e. _V ) -> <. ( F ` p ) , ( F ` q ) >. e. _V )
13	8, 11, 12	syl2anc 411	. . . . . . . . 9 |- ( ph -> <. ( F ` p ) , ( F ` q ) >. e. _V )
14		imasaddfnlemg.x	. . . . . . . . . . 11 |- ( ph -> .x. e. C )
15	9	a1i 9	. . . . . . . . . . 11 |- ( ph -> q e. _V )
16		ovexg 6001	. . . . . . . . . . 11 |- ( ( p e. _V /\ .x. e. C /\ q e. _V ) -> ( p .x. q ) e. _V )
17	6, 14, 15, 16	mp3an2i 1355	. . . . . . . . . 10 |- ( ph -> ( p .x. q ) e. _V )
18		fvexg 5618	. . . . . . . . . 10 |- ( ( F e. _V /\ ( p .x. q ) e. _V ) -> ( F ` ( p .x. q ) ) e. _V )
19	5, 17, 18	syl2anc 411	. . . . . . . . 9 |- ( ph -> ( F ` ( p .x. q ) ) e. _V )
20		relsnopg 4797	. . . . . . . . 9 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
21	13, 19, 20	syl2anc 411	. . . . . . . 8 |- ( ph -> Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
22	21	ralrimivw 2582	. . . . . . 7 |- ( ph -> A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
23		reliun 4814	. . . . . . 7 |- ( Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
24	22, 23	sylibr 134	. . . . . 6 |- ( ph -> Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
25	24	ralrimivw 2582	. . . . 5 |- ( ph -> A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
26		reliun 4814	. . . . 5 |- ( Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
27	25, 26	sylibr 134	. . . 4 |- ( ph -> Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
28		imasaddflem.a	. . . . 5 |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
29	28	releqd 4777	. . . 4 |- ( ph -> ( Rel .xb <-> Rel U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
30	27, 29	mpbird 167	. . 3 |- ( ph -> Rel .xb )
31		ffvelcdm 5736	. . . . . . . . . . . . . . . 16 |- ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B )
32		ffvelcdm 5736	. . . . . . . . . . . . . . . 16 |- ( ( F : V --> B /\ q e. V ) -> ( F ` q ) e. B )
33	31, 32	anim12dan 600	. . . . . . . . . . . . . . 15 |- ( ( F : V --> B /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
34	3, 33	sylan 283	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) )
35		opelxpi 4725	. . . . . . . . . . . . . 14 |- ( ( ( F ` p ) e. B /\ ( F ` q ) e. B ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
36	34, 35	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) )
37	19	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( F ` ( p .x. q ) ) e. _V )
38	36, 37	opelxpd 4726	. . . . . . . . . . . 12 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. ( ( B X. B ) X. _V ) )
39	38	snssd 3789	. . . . . . . . . . 11 |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
40	39	anassrs 400	. . . . . . . . . 10 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
41	40	iunssd 3987	. . . . . . . . 9 |- ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
42	41	iunssd 3987	. . . . . . . 8 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. _V ) )
43	28, 42	eqsstrd 3237	. . . . . . 7 |- ( ph -> .xb C_ ( ( B X. B ) X. _V ) )
44		dmss 4896	. . . . . . 7 |- ( .xb C_ ( ( B X. B ) X. _V ) -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
45	43, 44	syl 14	. . . . . 6 |- ( ph -> dom .xb C_ dom ( ( B X. B ) X. _V ) )
46		vn0m 3480	. . . . . . 7 |- E. w w e. _V
47		dmxpm 4917	. . . . . . 7 |- ( E. w w e. _V -> dom ( ( B X. B ) X. _V ) = ( B X. B ) )
48	46, 47	ax-mp 5	. . . . . 6 |- dom ( ( B X. B ) X. _V ) = ( B X. B )
49	45, 48	sseqtrdi 3249	. . . . 5 |- ( ph -> dom .xb C_ ( B X. B ) )
50		forn 5523	. . . . . . 7 |- ( F : V -onto-> B -> ran F = B )
51	1, 50	syl 14	. . . . . 6 |- ( ph -> ran F = B )
52	51	sqxpeqd 4719	. . . . 5 |- ( ph -> ( ran F X. ran F ) = ( B X. B ) )
53	49, 52	sseqtrrd 3240	. . . 4 |- ( ph -> dom .xb C_ ( ran F X. ran F ) )
54	28	eleq2d 2277	. . . . . . . . . . . . 13 |- ( ph -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
55	54	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
56		df-br 4060	. . . . . . . . . . . 12 |- ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb )
57		eliun 3945	. . . . . . . . . . . . 13 |- ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. p e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
58		eliun 3945	. . . . . . . . . . . . . 14 |- ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
59	58	rexbii 2515	. . . . . . . . . . . . 13 |- ( E. p e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
60	57, 59	bitr2i 185	. . . . . . . . . . . 12 |- ( E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
61	55, 56, 60	3bitr4g 223	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) )
62		vex 2779	. . . . . . . . . . . . . . . . . . 19 |- a e. _V
63		fvexg 5618	. . . . . . . . . . . . . . . . . . 19 |- ( ( F e. _V /\ a e. _V ) -> ( F ` a ) e. _V )
64	5, 62, 63	sylancl 413	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` a ) e. _V )
65		vex 2779	. . . . . . . . . . . . . . . . . . 19 |- b e. _V
66		fvexg 5618	. . . . . . . . . . . . . . . . . . 19 |- ( ( F e. _V /\ b e. _V ) -> ( F ` b ) e. _V )
67	5, 65, 66	sylancl 413	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F ` b ) e. _V )
68		opexg 4290	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` a ) e. _V /\ ( F ` b ) e. _V ) -> <. ( F ` a ) , ( F ` b ) >. e. _V )
69	64, 67, 68	syl2anc 411	. . . . . . . . . . . . . . . . 17 |- ( ph -> <. ( F ` a ) , ( F ` b ) >. e. _V )
70		vex 2779	. . . . . . . . . . . . . . . . 17 |- w e. _V
71		opexg 4290	. . . . . . . . . . . . . . . . 17 |- ( ( <. ( F ` a ) , ( F ` b ) >. e. _V /\ w e. _V ) -> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V )
72	69, 70, 71	sylancl 413	. . . . . . . . . . . . . . . 16 |- ( ph -> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V )
73		elsng 3658	. . . . . . . . . . . . . . . 16 |- ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. _V -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. ) )
74	72, 73	syl 14	. . . . . . . . . . . . . . 15 |- ( ph -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. ) )
75	74	3ad2ant1 1021	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. ) )
76		opthg 4300	. . . . . . . . . . . . . . . . 17 |- ( ( <. ( F ` a ) , ( F ` b ) >. e. _V /\ w e. _V ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. <-> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) ) )
77	69, 70, 76	sylancl 413	. . . . . . . . . . . . . . . 16 |- ( ph -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. <-> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) ) )
78	77	3ad2ant1 1021	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. <-> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) ) )
79		opthg 4300	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F ` a ) e. _V /\ ( F ` b ) e. _V ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
80	64, 67, 79	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
81	80	3ad2ant1 1021	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. <-> ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) )
82		imasaddf.e	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
83	81, 82	sylbid 150	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
84		eqeq2 2217	. . . . . . . . . . . . . . . . . 18 |- ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( a .x. b ) ) <-> w = ( F ` ( p .x. q ) ) ) )
85	84	biimprd 158	. . . . . . . . . . . . . . . . 17 |- ( ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) -> ( w = ( F ` ( p .x. q ) ) -> w = ( F ` ( a .x. b ) ) ) )
86	83, 85	syl6 33	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. -> ( w = ( F ` ( p .x. q ) ) -> w = ( F ` ( a .x. b ) ) ) ) )
87	86	impd 254	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( <. ( F ` a ) , ( F ` b ) >. = <. ( F ` p ) , ( F ` q ) >. /\ w = ( F ` ( p .x. q ) ) ) -> w = ( F ` ( a .x. b ) ) ) )
88	78, 87	sylbid 150	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. -> w = ( F ` ( a .x. b ) ) ) )
89	75, 88	sylbid 150	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
90	89	3expa 1206	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( p e. V /\ q e. V ) ) -> ( <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
91	90	rexlimdvva 2633	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( E. p e. V E. q e. V <. <. ( F ` a ) , ( F ` b ) >. , w >. e. { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> w = ( F ` ( a .x. b ) ) ) )
92	61, 91	sylbid 150	. . . . . . . . . 10 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
93	92	alrimiv 1898	. . . . . . . . 9 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
94		mo2icl 2959	. . . . . . . . 9 |- ( A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
95	93, 94	syl 14	. . . . . . . 8 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
96	95	ralrimivva 2590	. . . . . . 7 |- ( ph -> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
97		fofn 5522	. . . . . . . . . 10 |- ( F : V -onto-> B -> F Fn V )
98	1, 97	syl 14	. . . . . . . . 9 |- ( ph -> F Fn V )
99		opeq2 3834	. . . . . . . . . . . 12 |- ( z = ( F ` b ) -> <. ( F ` a ) , z >. = <. ( F ` a ) , ( F ` b ) >. )
100	99	breq1d 4069	. . . . . . . . . . 11 |- ( z = ( F ` b ) -> ( <. ( F ` a ) , z >. .xb w <-> <. ( F ` a ) , ( F ` b ) >. .xb w ) )
101	100	mobidv 2091	. . . . . . . . . 10 |- ( z = ( F ` b ) -> ( E* w <. ( F ` a ) , z >. .xb w <-> E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
102	101	ralrn 5741	. . . . . . . . 9 |- ( F Fn V -> ( A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
103	98, 102	syl 14	. . . . . . . 8 |- ( ph -> ( A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
104	103	ralbidv 2508	. . . . . . 7 |- ( ph -> ( A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w <-> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
105	96, 104	mpbird 167	. . . . . 6 |- ( ph -> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w )
106		opeq1 3833	. . . . . . . . . . 11 |- ( y = ( F ` a ) -> <. y , z >. = <. ( F ` a ) , z >. )
107	106	breq1d 4069	. . . . . . . . . 10 |- ( y = ( F ` a ) -> ( <. y , z >. .xb w <-> <. ( F ` a ) , z >. .xb w ) )
108	107	mobidv 2091	. . . . . . . . 9 |- ( y = ( F ` a ) -> ( E* w <. y , z >. .xb w <-> E* w <. ( F ` a ) , z >. .xb w ) )
109	108	ralbidv 2508	. . . . . . . 8 |- ( y = ( F ` a ) -> ( A. z e. ran F E* w <. y , z >. .xb w <-> A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
110	109	ralrn 5741	. . . . . . 7 |- ( F Fn V -> ( A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w <-> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
111	98, 110	syl 14	. . . . . 6 |- ( ph -> ( A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w <-> A. a e. V A. z e. ran F E* w <. ( F ` a ) , z >. .xb w ) )
112	105, 111	mpbird 167	. . . . 5 |- ( ph -> A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w )
113		breq1 4062	. . . . . . 7 |- ( x = <. y , z >. -> ( x .xb w <-> <. y , z >. .xb w ) )
114	113	mobidv 2091	. . . . . 6 |- ( x = <. y , z >. -> ( E* w x .xb w <-> E* w <. y , z >. .xb w ) )
115	114	ralxp 4839	. . . . 5 |- ( A. x e. ( ran F X. ran F ) E* w x .xb w <-> A. y e. ran F A. z e. ran F E* w <. y , z >. .xb w )
116	112, 115	sylibr 134	. . . 4 |- ( ph -> A. x e. ( ran F X. ran F ) E* w x .xb w )
117		ssralv 3265	. . . 4 |- ( dom .xb C_ ( ran F X. ran F ) -> ( A. x e. ( ran F X. ran F ) E* w x .xb w -> A. x e. dom .xb E* w x .xb w ) )
118	53, 116, 117	sylc 62	. . 3 |- ( ph -> A. x e. dom .xb E* w x .xb w )
119		dffun7 5317	. . 3 |- ( Fun .xb <-> ( Rel .xb /\ A. x e. dom .xb E* w x .xb w ) )
120	30, 118, 119	sylanbrc 417	. 2 |- ( ph -> Fun .xb )
121		eqimss2 3256	. . . . . . . . . . 11 |- ( .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
122	28, 121	syl 14	. . . . . . . . . 10 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
123		iunss 3982	. . . . . . . . . 10 |- ( U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb <-> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
124	122, 123	sylib 122	. . . . . . . . 9 |- ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
125		iunss 3982	. . . . . . . . . . 11 |- ( U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb <-> A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb )
126		opexg 4290	. . . . . . . . . . . . . . 15 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V )
127	13, 19, 126	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ph -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V )
128		snssg 3778	. . . . . . . . . . . . . 14 |- ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. _V -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb <-> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb ) )
129	127, 128	syl 14	. . . . . . . . . . . . 13 |- ( ph -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb <-> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb ) )
130		opeldmg 4902	. . . . . . . . . . . . . 14 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .x. q ) ) e. _V ) -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
131	13, 19, 130	syl2anc 411	. . . . . . . . . . . . 13 |- ( ph -> ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
132	129, 131	sylbird 170	. . . . . . . . . . . 12 |- ( ph -> ( { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
133	132	ralimdv 2576	. . . . . . . . . . 11 |- ( ph -> ( A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
134	125, 133	biimtrid 152	. . . . . . . . . 10 |- ( ph -> ( U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
135	134	ralimdv 2576	. . . . . . . . 9 |- ( ph -> ( A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ .xb -> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
136	124, 135	mpd 13	. . . . . . . 8 |- ( ph -> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb )
137		opeq2 3834	. . . . . . . . . . . 12 |- ( z = ( F ` q ) -> <. ( F ` p ) , z >. = <. ( F ` p ) , ( F ` q ) >. )
138	137	eleq1d 2276	. . . . . . . . . . 11 |- ( z = ( F ` q ) -> ( <. ( F ` p ) , z >. e. dom .xb <-> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
139	138	ralrn 5741	. . . . . . . . . 10 |- ( F Fn V -> ( A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
140	98, 139	syl 14	. . . . . . . . 9 |- ( ph -> ( A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
141	140	ralbidv 2508	. . . . . . . 8 |- ( ph -> ( A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb <-> A. p e. V A. q e. V <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
142	136, 141	mpbird 167	. . . . . . 7 |- ( ph -> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb )
143		opeq1 3833	. . . . . . . . . . 11 |- ( y = ( F ` p ) -> <. y , z >. = <. ( F ` p ) , z >. )
144	143	eleq1d 2276	. . . . . . . . . 10 |- ( y = ( F ` p ) -> ( <. y , z >. e. dom .xb <-> <. ( F ` p ) , z >. e. dom .xb ) )
145	144	ralbidv 2508	. . . . . . . . 9 |- ( y = ( F ` p ) -> ( A. z e. ran F <. y , z >. e. dom .xb <-> A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
146	145	ralrn 5741	. . . . . . . 8 |- ( F Fn V -> ( A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb <-> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
147	98, 146	syl 14	. . . . . . 7 |- ( ph -> ( A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb <-> A. p e. V A. z e. ran F <. ( F ` p ) , z >. e. dom .xb ) )
148	142, 147	mpbird 167	. . . . . 6 |- ( ph -> A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb )
149		eleq1 2270	. . . . . . 7 |- ( x = <. y , z >. -> ( x e. dom .xb <-> <. y , z >. e. dom .xb ) )
150	149	ralxp 4839	. . . . . 6 |- ( A. x e. ( ran F X. ran F ) x e. dom .xb <-> A. y e. ran F A. z e. ran F <. y , z >. e. dom .xb )
151	148, 150	sylibr 134	. . . . 5 |- ( ph -> A. x e. ( ran F X. ran F ) x e. dom .xb )
152		dfss3 3190	. . . . 5 |- ( ( ran F X. ran F ) C_ dom .xb <-> A. x e. ( ran F X. ran F ) x e. dom .xb )
153	151, 152	sylibr 134	. . . 4 |- ( ph -> ( ran F X. ran F ) C_ dom .xb )
154	52, 153	eqsstrrd 3238	. . 3 |- ( ph -> ( B X. B ) C_ dom .xb )
155	49, 154	eqssd 3218	. 2 |- ( ph -> dom .xb = ( B X. B ) )
156		df-fn 5293	. 2 |- ( .xb Fn ( B X. B ) <-> ( Fun .xb /\ dom .xb = ( B X. B ) ) )
157	120, 155, 156	sylanbrc 417	1 |- ( ph -> .xb Fn ( B X. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 981   A.wal 1371   = wceq 1373   E.wex 1516   E*wmo 2056   e. wcel 2178   A.wral 2486   E.wrex 2487   _Vcvv 2776   C_ wss 3174   {csn 3643   <.cop 3646   U_ciun 3941   class class class wbr 4059   X. cxp 4691   dom cdm 4693   ran crn 4694   Rel wrel 4698   Fun wfun 5284   Fn wfn 5285   -->wf 5286   -onto->wfo 5288   ` cfv 5290  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-coll 4175  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-csb 3102  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-iun 3943  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297  df-fv 5298  df-ov 5970

This theorem is referenced by:  imasaddvallemg  13262  imasaddflemg  13263  imasaddfn  13264  imasmulfn  13267