Theorem wfr3g 13956

Description: Functions defined by well founded recursion are identical up to relation, domain, and characteristic function.

Assertion

Ref	Expression
wfr3g	|- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> F = G)

Distinct variable groups:   x,A,y   x,F,y   x,G,y   x,H,y   x,R,y

Proof of Theorem wfr3g

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . . . . . . . 12 |- (z = w -> (F` z) = (F` w))
2		fveq2 4681	. . . . . . . . . . . 12 |- (z = w -> (G` z) = (G` w))
3	1, 2	eqeq12d 1899	. . . . . . . . . . 11 |- (z = w -> ((F` z) = (G` z) <-> (F` w) = (G` w)))
4	3	imbi2d 674	. . . . . . . . . 10 |- (z = w -> ((((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` z) = (G` z)) <-> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` w) = (G` w))))
5		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (F` y) = (F` z))
6		predeq3 13883	. . . . . . . . . . . . . . . . . . . . 21 |- (y = z -> Pred(R, A, y) = Pred(R, A, z))
7		reseq2 4219	. . . . . . . . . . . . . . . . . . . . 21 |- (Pred(R, A, y) = Pred(R, A, z) -> (F |` Pred(R, A, y)) = (F |` Pred(R, A, z)))
8	6, 7	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (F |` Pred(R, A, y)) = (F |` Pred(R, A, z)))
9	8	fveq2d 4685	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (H` (F |` Pred(R, A, y))) = (H` (F |` Pred(R, A, z))))
10	5, 9	eqeq12d 1899	. . . . . . . . . . . . . . . . . 18 |- (y = z -> ((F` y) = (H` (F |` Pred(R, A, y))) <-> (F` z) = (H` (F |` Pred(R, A, z)))))
11		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (G` y) = (G` z))
12		reseq2 4219	. . . . . . . . . . . . . . . . . . . . 21 |- (Pred(R, A, y) = Pred(R, A, z) -> (G |` Pred(R, A, y)) = (G |` Pred(R, A, z)))
13	6, 12	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (G |` Pred(R, A, y)) = (G |` Pred(R, A, z)))
14	13	fveq2d 4685	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (H` (G |` Pred(R, A, y))) = (H` (G |` Pred(R, A, z))))
15	11, 14	eqeq12d 1899	. . . . . . . . . . . . . . . . . 18 |- (y = z -> ((G` y) = (H` (G |` Pred(R, A, y))) <-> (G` z) = (H` (G |` Pred(R, A, z)))))
16	10, 15	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (y = z -> (((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y)))) <-> ((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z))))))
17	16	rcla4va 2378	. . . . . . . . . . . . . . . 16 |- ((z e. A /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> ((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))))
18		predss 13885	. . . . . . . . . . . . . . . . . . . . . . 23 |- Pred(R, A, z) C_ A
19		fvreseq 4772	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F Fn A /\ G Fn A) /\ Pred(R, A, z) C_ A) -> ((F |` Pred(R, A, z)) = (G |` Pred(R, A, z)) <-> A.w e. Pred (R, A, z)(F` w) = (G` w)))
20	18, 19	mpan2 760	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F Fn A /\ G Fn A) -> ((F |` Pred(R, A, z)) = (G |` Pred(R, A, z)) <-> A.w e. Pred (R, A, z)(F` w) = (G` w)))
21	20	biimpar 461	. . . . . . . . . . . . . . . . . . . . 21 |- (((F Fn A /\ G Fn A) /\ A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (F |` Pred(R, A, z)) = (G |` Pred(R, A, z)))
22	21	eqcomd 1889	. . . . . . . . . . . . . . . . . . . 20 |- (((F Fn A /\ G Fn A) /\ A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (G |` Pred(R, A, z)) = (F |` Pred(R, A, z)))
23	22	fveq2d 4685	. . . . . . . . . . . . . . . . . . 19 |- (((F Fn A /\ G Fn A) /\ A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (H` (G |` Pred(R, A, z))) = (H` (F |` Pred(R, A, z))))
24		eqtr3 1907	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` z) = (H` (F |` Pred(R, A, z))) /\ (H` (G |` Pred(R, A, z))) = (H` (F |` Pred(R, A, z)))) -> (F` z) = (H` (G |` Pred(R, A, z))))
25	24	ancoms 484	. . . . . . . . . . . . . . . . . . . . 21 |- (((H` (G |` Pred(R, A, z))) = (H` (F |` Pred(R, A, z))) /\ (F` z) = (H` (F |` Pred(R, A, z)))) -> (F` z) = (H` (G |` Pred(R, A, z))))
26		eqtr3 1907	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` z) = (H` (G |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))) -> (F` z) = (G` z))
27	26	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- ((F` z) = (H` (G |` Pred(R, A, z))) -> ((G` z) = (H` (G |` Pred(R, A, z))) -> (F` z) = (G` z)))
28	25, 27	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (((H` (G |` Pred(R, A, z))) = (H` (F |` Pred(R, A, z))) /\ (F` z) = (H` (F |` Pred(R, A, z)))) -> ((G` z) = (H` (G |` Pred(R, A, z))) -> (F` z) = (G` z)))
29	28	expimpd 404	. . . . . . . . . . . . . . . . . . 19 |- ((H` (G |` Pred(R, A, z))) = (H` (F |` Pred(R, A, z))) -> (((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))) -> (F` z) = (G` z)))
30	23, 29	syl 12	. . . . . . . . . . . . . . . . . 18 |- (((F Fn A /\ G Fn A) /\ A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))) -> (F` z) = (G` z)))
31	30	com12 14	. . . . . . . . . . . . . . . . 17 |- (((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))) -> (((F Fn A /\ G Fn A) /\ A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (F` z) = (G` z)))
32	31	exp3a 405	. . . . . . . . . . . . . . . 16 |- (((F` z) = (H` (F |` Pred(R, A, z))) /\ (G` z) = (H` (G |` Pred(R, A, z)))) -> ((F Fn A /\ G Fn A) -> (A.w e. Pred (R, A, z)(F` w) = (G` w) -> (F` z) = (G` z))))
33	17, 32	syl 12	. . . . . . . . . . . . . . 15 |- ((z e. A /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> ((F Fn A /\ G Fn A) -> (A.w e. Pred (R, A, z)(F` w) = (G` w) -> (F` z) = (G` z))))
34	33	ex 402	. . . . . . . . . . . . . 14 |- (z e. A -> (A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y)))) -> ((F Fn A /\ G Fn A) -> (A.w e. Pred (R, A, z)(F` w) = (G` w) -> (F` z) = (G` z)))))
35	34	com23 36	. . . . . . . . . . . . 13 |- (z e. A -> ((F Fn A /\ G Fn A) -> (A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y)))) -> (A.w e. Pred (R, A, z)(F` w) = (G` w) -> (F` z) = (G` z)))))
36	35	imp3a 388	. . . . . . . . . . . 12 |- (z e. A -> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (A.w e. Pred (R, A, z)(F` w) = (G` w) -> (F` z) = (G` z))))
37	36	a2d 16	. . . . . . . . . . 11 |- (z e. A -> ((((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.w e. Pred (R, A, z)(F` w) = (G` w)) -> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` z) = (G` z))))
38		ax-17 1317	. . . . . . . . . . . 12 |- (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.w((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))))
39	38	ra5 2539	. . . . . . . . . . 11 |- (A.w e. Pred (R, A, z)(((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` w) = (G` w)) -> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.w e. Pred (R, A, z)(F` w) = (G` w)))
40	37, 39	syl5 20	. . . . . . . . . 10 |- (z e. A -> (A.w e. Pred (R, A, z)(((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` w) = (G` w)) -> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` z) = (G` z))))
41	4, 40	wfis2g 13921	. . . . . . . . 9 |- ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> A.z e. A (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` z) = (G` z)))
42		ax-17 1317	. . . . . . . . . 10 |- (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.z((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))))
43	42	r19.21 13818	. . . . . . . . 9 |- (A.z e. A (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> (F` z) = (G` z)) <-> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.z e. A (F` z) = (G` z)))
44	41, 43	sylib 215	. . . . . . . 8 |- ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> A.z e. A (F` z) = (G` z)))
45	44	com12 14	. . . . . . 7 |- (((F Fn A /\ G Fn A) /\ A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y))))) -> ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> A.z e. A (F` z) = (G` z)))
46		r19.26 2219	. . . . . . 7 |- (A.y e. A ((F` y) = (H` (F |` Pred(R, A, y))) /\ (G` y) = (H` (G |` Pred(R, A, y)))) <-> (A.y e. A (F` y) = (H` (F |` Pred(R, A, y))) /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y)))))
47	45, 46	sylan2br 502	. . . . . 6 |- (((F Fn A /\ G Fn A) /\ (A.y e. A (F` y) = (H` (F |` Pred(R, A, y))) /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> A.z e. A (F` z) = (G` z)))
48	47	an4s 566	. . . . 5 |- (((F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> A.z e. A (F` z) = (G` z)))
49	48	com12 14	. . . 4 |- ((R We A /\ A.x e. A Pred(R, A, x) e. _V) -> (((F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> A.z e. A (F` z) = (G` z)))
50	49	3impib 1065	. . 3 |- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> A.z e. A (F` z) = (G` z))
51		eqid 1884	. . 3 |- A = A
52	50, 51	jctil 316	. 2 |- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> (A = A /\ A.z e. A (F` z) = (G` z)))
53		eqfnfv 4766	. . . 4 |- ((F Fn A /\ G Fn A) -> (F = G <-> (A = A /\ A.z e. A (F` z) = (G` z))))
54	53	ad2ant2r 445	. . 3 |- (((F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> (F = G <-> (A = A /\ A.z e. A (F` z) = (G` z))))
55	54	3adant1 894	. 2 |- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> (F = G <-> (A = A /\ A.z e. A (F` z) = (G` z))))
56	52, 55	mpbird 213	1 |- (((R We A /\ A.x e. A Pred(R, A, x) e. _V) /\ (F Fn A /\ A.y e. A (F` y) = (H` (F |` Pred(R, A, y)))) /\ (G Fn A /\ A.y e. A (G` y) = (H` (G |` Pred(R, A, y))))) -> F = G)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593   We wwe 3624   |` cres 3988   Fn wfn 3993  ` cfv 3998  Predcpred 13879

This theorem is referenced by:  wfrlem5 13961  wfr3 13975

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-pred 13880

Copyright terms: Public domain