Theorem imasaddfnlemg 12735

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 5439	. . . . . . . . . . . . 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 5747	. . . . . . . . . . 11 |- ( ph -> F e. _V )
6		vex 2741	. . . . . . . . . . 11 |- p e. _V
7		fvexg 5535	. . . . . . . . . . 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 2741	. . . . . . . . . . 11 |- q e. _V
10		fvexg 5535	. . . . . . . . . . 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 4229	. . . . . . . . . 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 5909	. . . . . . . . . . 11 |- ( ( p e. _V /\ .x. e. C /\ q e. _V ) -> ( p .x. q ) e. _V )
17	6, 14, 15, 16	mp3an2i 1342	. . . . . . . . . 10 |- ( ph -> ( p .x. q ) e. _V )
18		fvexg 5535	. . . . . . . . . 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 4731	. . . . . . . . 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 2551	. . . . . . 7 |- ( ph -> A. q e. V Rel { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
23		reliun 4748	. . . . . . 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 2551	. . . . 5 |- ( ph -> A. p e. V Rel U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
26		reliun 4748	. . . . 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 4711	. . . 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 5650	. . . . . . . . . . . . . . . 16 |- ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B )
32		ffvelcdm 5650	. . . . . . . . . . . . . . . 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 4659	. . . . . . . . . . . . . 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 4660	. . . . . . . . . . . 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 3738	. . . . . . . . . . 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 3933	. . . . . . . . 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 3933	. . . . . . . 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 3192	. . . . . . 7 |- ( ph -> .xb C_ ( ( B X. B ) X. _V ) )
44		dmss 4827	. . . . . . 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 3435	. . . . . . 7 |- E. w w e. _V
47		dmxpm 4848	. . . . . . 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 3204	. . . . 5 |- ( ph -> dom .xb C_ ( B X. B ) )
50		forn 5442	. . . . . . 7 |- ( F : V -onto-> B -> ran F = B )
51	1, 50	syl 14	. . . . . 6 |- ( ph -> ran F = B )
52	51	sqxpeqd 4653	. . . . 5 |- ( ph -> ( ran F X. ran F ) = ( B X. B ) )
53	49, 52	sseqtrrd 3195	. . . 4 |- ( ph -> dom .xb C_ ( ran F X. ran F ) )
54	28	eleq2d 2247	. . . . . . . . . . . . 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 4005	. . . . . . . . . . . 12 |- ( <. ( F ` a ) , ( F ` b ) >. .xb w <-> <. <. ( F ` a ) , ( F ` b ) >. , w >. e. .xb )
57		eliun 3891	. . . . . . . . . . . . 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 3891	. . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . 19 |- a e. _V
63		fvexg 5535	. . . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . 19 |- b e. _V
66		fvexg 5535	. . . . . . . . . . . . . . . . . . 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 4229	. . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . 17 |- w e. _V
71		opexg 4229	. . . . . . . . . . . . . . . . 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 3608	. . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . 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 4239	. . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . 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 2187	. . . . . . . . . . . . . . . . . 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 1203	. . . . . . . . . . . 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 2602	. . . . . . . . . . 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 1874	. . . . . . . . 9 |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> A. w ( <. ( F ` a ) , ( F ` b ) >. .xb w -> w = ( F ` ( a .x. b ) ) ) )
94		mo2icl 2917	. . . . . . . . 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 2559	. . . . . . 7 |- ( ph -> A. a e. V A. b e. V E* w <. ( F ` a ) , ( F ` b ) >. .xb w )
97		fofn 5441	. . . . . . . . . 10 |- ( F : V -onto-> B -> F Fn V )
98	1, 97	syl 14	. . . . . . . . 9 |- ( ph -> F Fn V )
99		opeq2 3780	. . . . . . . . . . . 12 |- ( z = ( F ` b ) -> <. ( F ` a ) , z >. = <. ( F ` a ) , ( F ` b ) >. )
100	99	breq1d 4014	. . . . . . . . . . 11 |- ( z = ( F ` b ) -> ( <. ( F ` a ) , z >. .xb w <-> <. ( F ` a ) , ( F ` b ) >. .xb w ) )
101	100	mobidv 2062	. . . . . . . . . 10 |- ( z = ( F ` b ) -> ( E* w <. ( F ` a ) , z >. .xb w <-> E* w <. ( F ` a ) , ( F ` b ) >. .xb w ) )
102	101	ralrn 5655	. . . . . . . . 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 2477	. . . . . . 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 3779	. . . . . . . . . . 11 |- ( y = ( F ` a ) -> <. y , z >. = <. ( F ` a ) , z >. )
107	106	breq1d 4014	. . . . . . . . . 10 |- ( y = ( F ` a ) -> ( <. y , z >. .xb w <-> <. ( F ` a ) , z >. .xb w ) )
108	107	mobidv 2062	. . . . . . . . 9 |- ( y = ( F ` a ) -> ( E* w <. y , z >. .xb w <-> E* w <. ( F ` a ) , z >. .xb w ) )
109	108	ralbidv 2477	. . . . . . . 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 5655	. . . . . . 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 4007	. . . . . . 7 |- ( x = <. y , z >. -> ( x .xb w <-> <. y , z >. .xb w ) )
114	113	mobidv 2062	. . . . . 6 |- ( x = <. y , z >. -> ( E* w x .xb w <-> E* w <. y , z >. .xb w ) )
115	114	ralxp 4771	. . . . 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 3220	. . . 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 5244	. . 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 3211	. . . . . . . . . . 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 3928	. . . . . . . . . 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 3928	. . . . . . . . . . 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 4229	. . . . . . . . . . . . . . 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 3727	. . . . . . . . . . . . . 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 4833	. . . . . . . . . . . . . 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 2545	. . . . . . . . . . 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 2545	. . . . . . . . 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 3780	. . . . . . . . . . . 12 |- ( z = ( F ` q ) -> <. ( F ` p ) , z >. = <. ( F ` p ) , ( F ` q ) >. )
138	137	eleq1d 2246	. . . . . . . . . . 11 |- ( z = ( F ` q ) -> ( <. ( F ` p ) , z >. e. dom .xb <-> <. ( F ` p ) , ( F ` q ) >. e. dom .xb ) )
139	138	ralrn 5655	. . . . . . . . . 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 2477	. . . . . . . 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 3779	. . . . . . . . . . 11 |- ( y = ( F ` p ) -> <. y , z >. = <. ( F ` p ) , z >. )
144	143	eleq1d 2246	. . . . . . . . . 10 |- ( y = ( F ` p ) -> ( <. y , z >. e. dom .xb <-> <. ( F ` p ) , z >. e. dom .xb ) )
145	144	ralbidv 2477	. . . . . . . . 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 5655	. . . . . . . 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 2240	. . . . . . 7 |- ( x = <. y , z >. -> ( x e. dom .xb <-> <. y , z >. e. dom .xb ) )
150	149	ralxp 4771	. . . . . 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 3146	. . . . 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 3193	. . 3 |- ( ph -> ( B X. B ) C_ dom .xb )
155	49, 154	eqssd 3173	. 2 |- ( ph -> dom .xb = ( B X. B ) )
156		df-fn 5220	. 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 978   A.wal 1351   = wceq 1353   E.wex 1492   E*wmo 2027   e. wcel 2148   A.wral 2455   E.wrex 2456   _Vcvv 2738   C_ wss 3130   {csn 3593   <.cop 3596   U_ciun 3887   class class class wbr 4004   X. cxp 4625   dom cdm 4627   ran crn 4628   Rel wrel 4632   Fun wfun 5211   Fn wfn 5212   -->wf 5213   -onto->wfo 5215   ` cfv 5217  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878

This theorem is referenced by:  imasaddvallemg  12736  imasaddflemg  12737  imasaddfn  12738  imasmulfn  12741