Theorem bnj1379 29714

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj1379.1	|- ( ph <-> A. f e. A Fun f )
bnj1379.2	|- D = ( dom f i^i dom g )
bnj1379.3	|- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
bnj1379.5	|- ( ch <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )
bnj1379.6	|- ( th <-> ( ch /\ f e. A /\ <. x , y >. e. f ) )
bnj1379.7	|- ( ta <-> ( th /\ g e. A /\ <. x , z >. e. g ) )

Assertion

Ref	Expression
bnj1379	|- ( ps -> Fun U. A )

Distinct variable groups:   A, f, g, x, y, z   x, D   ph, g   ps, x, y, z

Allowed substitution hints:   ph( x, y, z, f)   ps( f, g)   ch( x, y, z, f, g)   th( x, y, z, f, g)   ta( x, y, z, f, g)   D( y, z, f, g)

Proof of Theorem bnj1379

Step	Hyp	Ref	Expression
1		bnj1379.3	. . . . 5 |- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )
2		bnj1379.1	. . . . . . . 8 |- ( ph <-> A. f e. A Fun f )
3	2	bnj1095 29665	. . . . . . 7 |- ( ph -> A. f ph )
4	3	nfi 1682	. . . . . 6 |- F/ f ph
5		nfra1 2785	. . . . . 6 |- F/ f A. f e. A A. g e. A ( f |` D ) = ( g |` D )
6	4, 5	nfan 2031	. . . . 5 |- F/ f ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
7	1, 6	nfxfr 1704	. . . 4 |- F/ f ps
8	2	bnj946 29658	. . . . . . . 8 |- ( ph <-> A. f ( f e. A -> Fun f ) )
9	8	biimpi 199	. . . . . . 7 |- ( ph -> A. f ( f e. A -> Fun f ) )
10	9	19.21bi 1967	. . . . . 6 |- ( ph -> ( f e. A -> Fun f ) )
11	1, 10	bnj832 29640	. . . . 5 |- ( ps -> ( f e. A -> Fun f ) )
12		funrel 5606	. . . . 5 |- ( Fun f -> Rel f )
13	11, 12	syl6 33	. . . 4 |- ( ps -> ( f e. A -> Rel f ) )
14	7, 13	ralrimi 2800	. . 3 |- ( ps -> A. f e. A Rel f )
15		reluni 4961	. . 3 |- ( Rel U. A <-> A. f e. A Rel f )
16	14, 15	sylibr 217	. 2 |- ( ps -> Rel U. A )
17		bnj1379.5	. . . . . 6 |- ( ch <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )
18		eluni2 4194	. . . . . . . . . . . 12 |- ( <. x , y >. e. U. A <-> E. f e. A <. x , y >. e. f )
19	18	biimpi 199	. . . . . . . . . . 11 |- ( <. x , y >. e. U. A -> E. f e. A <. x , y >. e. f )
20	19	bnj1196 29678	. . . . . . . . . 10 |- ( <. x , y >. e. U. A -> E. f ( f e. A /\ <. x , y >. e. f ) )
21	17, 20	bnj836 29643	. . . . . . . . 9 |- ( ch -> E. f ( f e. A /\ <. x , y >. e. f ) )
22		bnj1379.6	. . . . . . . . 9 |- ( th <-> ( ch /\ f e. A /\ <. x , y >. e. f ) )
23		nfv 1769	. . . . . . . . . . . 12 |- F/ f <. x , y >. e. U. A
24		nfv 1769	. . . . . . . . . . . 12 |- F/ f <. x , z >. e. U. A
25	7, 23, 24	nf3an 2033	. . . . . . . . . . 11 |- F/ f ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A )
26	17, 25	nfxfr 1704	. . . . . . . . . 10 |- F/ f ch
27	26	nfri 1972	. . . . . . . . 9 |- ( ch -> A. f ch )
28	21, 22, 27	bnj1345 29708	. . . . . . . 8 |- ( ch -> E. f th )
29	17	simp3bi 1047	. . . . . . . . . . . . 13 |- ( ch -> <. x , z >. e. U. A )
30	22, 29	bnj835 29642	. . . . . . . . . . . 12 |- ( th -> <. x , z >. e. U. A )
31		eluni2 4194	. . . . . . . . . . . . . 14 |- ( <. x , z >. e. U. A <-> E. g e. A <. x , z >. e. g )
32	31	biimpi 199	. . . . . . . . . . . . 13 |- ( <. x , z >. e. U. A -> E. g e. A <. x , z >. e. g )
33	32	bnj1196 29678	. . . . . . . . . . . 12 |- ( <. x , z >. e. U. A -> E. g ( g e. A /\ <. x , z >. e. g ) )
34	30, 33	syl 17	. . . . . . . . . . 11 |- ( th -> E. g ( g e. A /\ <. x , z >. e. g ) )
35		bnj1379.7	. . . . . . . . . . 11 |- ( ta <-> ( th /\ g e. A /\ <. x , z >. e. g ) )
36		nfv 1769	. . . . . . . . . . . . . . . . . 18 |- F/ g ph
37		nfra2 2790	. . . . . . . . . . . . . . . . . 18 |- F/ g A. f e. A A. g e. A ( f |` D ) = ( g |` D )
38	36, 37	nfan 2031	. . . . . . . . . . . . . . . . 17 |- F/ g ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
39	1, 38	nfxfr 1704	. . . . . . . . . . . . . . . 16 |- F/ g ps
40		nfv 1769	. . . . . . . . . . . . . . . 16 |- F/ g <. x , y >. e. U. A
41		nfv 1769	. . . . . . . . . . . . . . . 16 |- F/ g <. x , z >. e. U. A
42	39, 40, 41	nf3an 2033	. . . . . . . . . . . . . . 15 |- F/ g ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A )
43	17, 42	nfxfr 1704	. . . . . . . . . . . . . 14 |- F/ g ch
44		nfv 1769	. . . . . . . . . . . . . 14 |- F/ g f e. A
45		nfv 1769	. . . . . . . . . . . . . 14 |- F/ g <. x , y >. e. f
46	43, 44, 45	nf3an 2033	. . . . . . . . . . . . 13 |- F/ g ( ch /\ f e. A /\ <. x , y >. e. f )
47	22, 46	nfxfr 1704	. . . . . . . . . . . 12 |- F/ g th
48	47	nfri 1972	. . . . . . . . . . 11 |- ( th -> A. g th )
49	34, 35, 48	bnj1345 29708	. . . . . . . . . 10 |- ( th -> E. g ta )
50	1	simprbi 471	. . . . . . . . . . . . . . . . . 18 |- ( ps -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
51	17, 50	bnj835 29642	. . . . . . . . . . . . . . . . 17 |- ( ch -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
52	22, 51	bnj835 29642	. . . . . . . . . . . . . . . 16 |- ( th -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
53	35, 52	bnj835 29642	. . . . . . . . . . . . . . 15 |- ( ta -> A. f e. A A. g e. A ( f |` D ) = ( g |` D ) )
54	22, 35	bnj1219 29684	. . . . . . . . . . . . . . 15 |- ( ta -> f e. A )
55	53, 54	bnj1294 29701	. . . . . . . . . . . . . 14 |- ( ta -> A. g e. A ( f |` D ) = ( g |` D ) )
56	35	simp2bi 1046	. . . . . . . . . . . . . 14 |- ( ta -> g e. A )
57	55, 56	bnj1294 29701	. . . . . . . . . . . . 13 |- ( ta -> ( f |` D ) = ( g |` D ) )
58	57	fveq1d 5881	. . . . . . . . . . . 12 |- ( ta -> ( ( f |` D ) ` x ) = ( ( g |` D ) ` x ) )
59	22	simp3bi 1047	. . . . . . . . . . . . . . . . 17 |- ( th -> <. x , y >. e. f )
60	35, 59	bnj835 29642	. . . . . . . . . . . . . . . 16 |- ( ta -> <. x , y >. e. f )
61		vex 3034	. . . . . . . . . . . . . . . . 17 |- x e. _V
62		vex 3034	. . . . . . . . . . . . . . . . 17 |- y e. _V
63	61, 62	opeldm 5044	. . . . . . . . . . . . . . . 16 |- ( <. x , y >. e. f -> x e. dom f )
64	60, 63	syl 17	. . . . . . . . . . . . . . 15 |- ( ta -> x e. dom f )
65		vex 3034	. . . . . . . . . . . . . . . . 17 |- z e. _V
66	61, 65	opeldm 5044	. . . . . . . . . . . . . . . 16 |- ( <. x , z >. e. g -> x e. dom g )
67	35, 66	bnj837 29644	. . . . . . . . . . . . . . 15 |- ( ta -> x e. dom g )
68	64, 67	elind 3609	. . . . . . . . . . . . . 14 |- ( ta -> x e. ( dom f i^i dom g ) )
69		bnj1379.2	. . . . . . . . . . . . . 14 |- D = ( dom f i^i dom g )
70	68, 69	syl6eleqr 2560	. . . . . . . . . . . . 13 |- ( ta -> x e. D )
71		fvres 5893	. . . . . . . . . . . . 13 |- ( x e. D -> ( ( f |` D ) ` x ) = ( f ` x ) )
72	70, 71	syl 17	. . . . . . . . . . . 12 |- ( ta -> ( ( f |` D ) ` x ) = ( f ` x ) )
73		fvres 5893	. . . . . . . . . . . . 13 |- ( x e. D -> ( ( g |` D ) ` x ) = ( g ` x ) )
74	70, 73	syl 17	. . . . . . . . . . . 12 |- ( ta -> ( ( g |` D ) ` x ) = ( g ` x ) )
75	58, 72, 74	3eqtr3d 2513	. . . . . . . . . . 11 |- ( ta -> ( f ` x ) = ( g ` x ) )
76	2	biimpi 199	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. f e. A Fun f )
77	1, 76	bnj832 29640	. . . . . . . . . . . . . . . 16 |- ( ps -> A. f e. A Fun f )
78	17, 77	bnj835 29642	. . . . . . . . . . . . . . 15 |- ( ch -> A. f e. A Fun f )
79	22, 78	bnj835 29642	. . . . . . . . . . . . . 14 |- ( th -> A. f e. A Fun f )
80	35, 79	bnj835 29642	. . . . . . . . . . . . 13 |- ( ta -> A. f e. A Fun f )
81	80, 54	bnj1294 29701	. . . . . . . . . . . 12 |- ( ta -> Fun f )
82		funopfv 5918	. . . . . . . . . . . 12 |- ( Fun f -> ( <. x , y >. e. f -> ( f ` x ) = y ) )
83	81, 60, 82	sylc 61	. . . . . . . . . . 11 |- ( ta -> ( f ` x ) = y )
84		funeq 5608	. . . . . . . . . . . . . . 15 |- ( f = g -> ( Fun f <-> Fun g ) )
85	84	cbvralv 3005	. . . . . . . . . . . . . 14 |- ( A. f e. A Fun f <-> A. g e. A Fun g )
86	80, 85	sylib 201	. . . . . . . . . . . . 13 |- ( ta -> A. g e. A Fun g )
87	86, 56	bnj1294 29701	. . . . . . . . . . . 12 |- ( ta -> Fun g )
88	35	simp3bi 1047	. . . . . . . . . . . 12 |- ( ta -> <. x , z >. e. g )
89		funopfv 5918	. . . . . . . . . . . 12 |- ( Fun g -> ( <. x , z >. e. g -> ( g ` x ) = z ) )
90	87, 88, 89	sylc 61	. . . . . . . . . . 11 |- ( ta -> ( g ` x ) = z )
91	75, 83, 90	3eqtr3d 2513	. . . . . . . . . 10 |- ( ta -> y = z )
92	49, 91	bnj593 29627	. . . . . . . . 9 |- ( th -> E. g y = z )
93	92	bnj937 29655	. . . . . . . 8 |- ( th -> y = z )
94	28, 93	bnj593 29627	. . . . . . 7 |- ( ch -> E. f y = z )
95	94	bnj937 29655	. . . . . 6 |- ( ch -> y = z )
96	17, 95	sylbir 218	. . . . 5 |- ( ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z )
97	96	3expib 1234	. . . 4 |- ( ps -> ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
98	97	alrimivv 1782	. . 3 |- ( ps -> A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
99	98	alrimiv 1781	. 2 |- ( ps -> A. x A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) )
100		dffun4 5601	. 2 |- ( Fun U. A <-> ( Rel U. A /\ A. x A. y A. z ( ( <. x , y >. e. U. A /\ <. x , z >. e. U. A ) -> y = z ) ) )
101	16, 99, 100	sylanbrc 677	1 |- ( ps -> Fun U. A )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   A.wral 2756   E.wrex 2757   i^i cin 3389   <.cop 3965   U.cuni 4190   dom cdm 4839   |` cres 4841   Rel wrel 4844   Fun wfun 5583   ` cfv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-res 4851  df-iota 5553  df-fun 5591  df-fv 5597

This theorem is referenced by:  bnj1383  29715