Theorem tz7.48lem 5164

Description: A way of showing an ordinal function is one-to-one.

Hypothesis

Ref	Expression
tz7.48.1	|- F Fn On

Assertion

Ref	Expression
tz7.48lem	|- ((A C_ On /\ A.x e. A A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` A))

Distinct variable groups:   x,y,F   x,A,y

Proof of Theorem tz7.48lem

Step	Hyp	Ref	Expression
1		fvres 4691	. . . . . . . . . . . 12 |- (x e. A -> ((F |` A)` x) = (F` x))
2		fvres 4691	. . . . . . . . . . . 12 |- (y e. A -> ((F |` A)` y) = (F` y))
3	1, 2	eqeqan12d 1901	. . . . . . . . . . 11 |- ((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) <-> (F` x) = (F` y)))
4	3	ad2antrl 442	. . . . . . . . . 10 |- ((A C_ On /\ ((x e. A /\ y e. A) /\ ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))))) -> (((F |` A)` x) = ((F |` A)` y) <-> (F` x) = (F` y)))
5		ssel 2615	. . . . . . . . . . . . 13 |- (A C_ On -> (x e. A -> x e. On))
6		ssel 2615	. . . . . . . . . . . . 13 |- (A C_ On -> (y e. A -> y e. On))
7	5, 6	anim12d 617	. . . . . . . . . . . 12 |- (A C_ On -> ((x e. A /\ y e. A) -> (x e. On /\ y e. On)))
8		pm3.48 616	. . . . . . . . . . . . . . 15 |- (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> ((x e. y \/ y e. x) -> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y))))
9		oridm 262	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> -. (F` x) = (F` y))
10		eqcom 1886	. . . . . . . . . . . . . . . . . 18 |- ((F` x) = (F` y) <-> (F` y) = (F` x))
11	10	notbii 204	. . . . . . . . . . . . . . . . 17 |- (-. (F` x) = (F` y) <-> -. (F` y) = (F` x))
12	11	orbi1i 276	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
13	9, 12	bitr3i 192	. . . . . . . . . . . . . . 15 |- (-. (F` x) = (F` y) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
14	8, 13	syl6ibr 230	. . . . . . . . . . . . . 14 |- (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> ((x e. y \/ y e. x) -> -. (F` x) = (F` y)))
15	14	con2d 107	. . . . . . . . . . . . 13 |- (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> ((F` x) = (F` y) -> -. (x e. y \/ y e. x)))
16		ordtri3 3697	. . . . . . . . . . . . . . 15 |- ((Ord x /\ Ord y) -> (x = y <-> -. (x e. y \/ y e. x)))
17	16	biimprd 171	. . . . . . . . . . . . . 14 |- ((Ord x /\ Ord y) -> (-. (x e. y \/ y e. x) -> x = y))
18		eloni 3667	. . . . . . . . . . . . . 14 |- (x e. On -> Ord x)
19		eloni 3667	. . . . . . . . . . . . . 14 |- (y e. On -> Ord y)
20	17, 18, 19	syl2an 503	. . . . . . . . . . . . 13 |- ((x e. On /\ y e. On) -> (-. (x e. y \/ y e. x) -> x = y))
21	15, 20	syl9r 72	. . . . . . . . . . . 12 |- ((x e. On /\ y e. On) -> (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> ((F` x) = (F` y) -> x = y)))
22	7, 21	syl6 25	. . . . . . . . . . 11 |- (A C_ On -> ((x e. A /\ y e. A) -> (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> ((F` x) = (F` y) -> x = y))))
23	22	imp32 390	. . . . . . . . . 10 |- ((A C_ On /\ ((x e. A /\ y e. A) /\ ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))))) -> ((F` x) = (F` y) -> x = y))
24	4, 23	sylbid 220	. . . . . . . . 9 |- ((A C_ On /\ ((x e. A /\ y e. A) /\ ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))))) -> (((F |` A)` x) = ((F |` A)` y) -> x = y))
25	24	exp32 408	. . . . . . . 8 |- (A C_ On -> ((x e. A /\ y e. A) -> (((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> (((F |` A)` x) = ((F |` A)` y) -> x = y))))
26	25	a2d 16	. . . . . . 7 |- (A C_ On -> (((x e. A /\ y e. A) -> ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y)))) -> ((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) -> x = y))))
27	26	alimdv 1668	. . . . . 6 |- (A C_ On -> (A.y((x e. A /\ y e. A) -> ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y)))) -> A.y((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) -> x = y))))
28	27	alimdv 1668	. . . . 5 |- (A C_ On -> (A.xA.y((x e. A /\ y e. A) -> ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y)))) -> A.xA.y((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) -> x = y))))
29		r2al 2136	. . . . 5 |- (A.x e. A A.y e. A ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) <-> A.xA.y((x e. A /\ y e. A) -> ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y)))))
30		r2al 2136	. . . . 5 |- (A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y) <-> A.xA.y((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) -> x = y)))
31	28, 29, 30	3imtr4g 612	. . . 4 |- (A C_ On -> (A.x e. A A.y e. A ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) -> A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)))
32		simpl 346	. . . . . . . . . 10 |- ((x e. A /\ y e. A) -> x e. A)
33	32	anim1i 361	. . . . . . . . 9 |- (((x e. A /\ y e. A) /\ y e. x) -> (x e. A /\ y e. x))
34	33	imim1i 19	. . . . . . . 8 |- (((x e. A /\ y e. x) -> -. (F` x) = (F` y)) -> (((x e. A /\ y e. A) /\ y e. x) -> -. (F` x) = (F` y)))
35	34	exp3a 405	. . . . . . 7 |- (((x e. A /\ y e. x) -> -. (F` x) = (F` y)) -> ((x e. A /\ y e. A) -> (y e. x -> -. (F` x) = (F` y))))
36	35	2alimi 1339	. . . . . 6 |- (A.xA.y((x e. A /\ y e. x) -> -. (F` x) = (F` y)) -> A.xA.y((x e. A /\ y e. A) -> (y e. x -> -. (F` x) = (F` y))))
37		r2al 2136	. . . . . 6 |- (A.x e. A A.y e. x -. (F` x) = (F` y) <-> A.xA.y((x e. A /\ y e. x) -> -. (F` x) = (F` y)))
38		r2al 2136	. . . . . 6 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) <-> A.xA.y((x e. A /\ y e. A) -> (y e. x -> -. (F` x) = (F` y))))
39	36, 37, 38	3imtr4i 236	. . . . 5 |- (A.x e. A A.y e. x -. (F` x) = (F` y) -> A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)))
40		eleq1 1957	. . . . . . . . . . . 12 |- (y = w -> (y e. x <-> w e. x))
41		fveq2 4681	. . . . . . . . . . . . . 14 |- (y = w -> (F` y) = (F` w))
42	41	eqeq2d 1895	. . . . . . . . . . . . 13 |- (y = w -> ((F` x) = (F` y) <-> (F` x) = (F` w)))
43	42	notbid 673	. . . . . . . . . . . 12 |- (y = w -> (-. (F` x) = (F` y) <-> -. (F` x) = (F` w)))
44	40, 43	imbi12d 688	. . . . . . . . . . 11 |- (y = w -> ((y e. x -> -. (F` x) = (F` y)) <-> (w e. x -> -. (F` x) = (F` w))))
45	44	cbvralv 2280	. . . . . . . . . 10 |- (A.y e. A (y e. x -> -. (F` x) = (F` y)) <-> A.w e. A (w e. x -> -. (F` x) = (F` w)))
46	45	ralbii 2127	. . . . . . . . 9 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) <-> A.x e. A A.w e. A (w e. x -> -. (F` x) = (F` w)))
47		eleq2 1958	. . . . . . . . . . . 12 |- (x = z -> (w e. x <-> w e. z))
48		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = z -> (F` x) = (F` z))
49	48	eqeq1d 1892	. . . . . . . . . . . . 13 |- (x = z -> ((F` x) = (F` w) <-> (F` z) = (F` w)))
50	49	notbid 673	. . . . . . . . . . . 12 |- (x = z -> (-. (F` x) = (F` w) <-> -. (F` z) = (F` w)))
51	47, 50	imbi12d 688	. . . . . . . . . . 11 |- (x = z -> ((w e. x -> -. (F` x) = (F` w)) <-> (w e. z -> -. (F` z) = (F` w))))
52	51	ralbidv 2123	. . . . . . . . . 10 |- (x = z -> (A.w e. A (w e. x -> -. (F` x) = (F` w)) <-> A.w e. A (w e. z -> -. (F` z) = (F` w))))
53	52	cbvralv 2280	. . . . . . . . 9 |- (A.x e. A A.w e. A (w e. x -> -. (F` x) = (F` w)) <-> A.z e. A A.w e. A (w e. z -> -. (F` z) = (F` w)))
54		eleq1 1957	. . . . . . . . . . . . 13 |- (w = x -> (w e. z <-> x e. z))
55		fveq2 4681	. . . . . . . . . . . . . . 15 |- (w = x -> (F` w) = (F` x))
56	55	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (w = x -> ((F` z) = (F` w) <-> (F` z) = (F` x)))
57	56	notbid 673	. . . . . . . . . . . . 13 |- (w = x -> (-. (F` z) = (F` w) <-> -. (F` z) = (F` x)))
58	54, 57	imbi12d 688	. . . . . . . . . . . 12 |- (w = x -> ((w e. z -> -. (F` z) = (F` w)) <-> (x e. z -> -. (F` z) = (F` x))))
59	58	cbvralv 2280	. . . . . . . . . . 11 |- (A.w e. A (w e. z -> -. (F` z) = (F` w)) <-> A.x e. A (x e. z -> -. (F` z) = (F` x)))
60	59	ralbii 2127	. . . . . . . . . 10 |- (A.z e. A A.w e. A (w e. z -> -. (F` z) = (F` w)) <-> A.z e. A A.x e. A (x e. z -> -. (F` z) = (F` x)))
61		eleq2 1958	. . . . . . . . . . . . 13 |- (z = y -> (x e. z <-> x e. y))
62		fveq2 4681	. . . . . . . . . . . . . . 15 |- (z = y -> (F` z) = (F` y))
63	62	eqeq1d 1892	. . . . . . . . . . . . . 14 |- (z = y -> ((F` z) = (F` x) <-> (F` y) = (F` x)))
64	63	notbid 673	. . . . . . . . . . . . 13 |- (z = y -> (-. (F` z) = (F` x) <-> -. (F` y) = (F` x)))
65	61, 64	imbi12d 688	. . . . . . . . . . . 12 |- (z = y -> ((x e. z -> -. (F` z) = (F` x)) <-> (x e. y -> -. (F` y) = (F` x))))
66	65	ralbidv 2123	. . . . . . . . . . 11 |- (z = y -> (A.x e. A (x e. z -> -. (F` z) = (F` x)) <-> A.x e. A (x e. y -> -. (F` y) = (F` x))))
67	66	cbvralv 2280	. . . . . . . . . 10 |- (A.z e. A A.x e. A (x e. z -> -. (F` z) = (F` x)) <-> A.y e. A A.x e. A (x e. y -> -. (F` y) = (F` x)))
68	60, 67	bitri 190	. . . . . . . . 9 |- (A.z e. A A.w e. A (w e. z -> -. (F` z) = (F` w)) <-> A.y e. A A.x e. A (x e. y -> -. (F` y) = (F` x)))
69	46, 53, 68	3bitri 194	. . . . . . . 8 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) <-> A.y e. A A.x e. A (x e. y -> -. (F` y) = (F` x)))
70		ralcom2 2244	. . . . . . . 8 |- (A.y e. A A.x e. A (x e. y -> -. (F` y) = (F` x)) -> A.x e. A A.y e. A (x e. y -> -. (F` y) = (F` x)))
71	69, 70	sylbi 216	. . . . . . 7 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) -> A.x e. A A.y e. A (x e. y -> -. (F` y) = (F` x)))
72	71	ancri 321	. . . . . 6 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) -> (A.x e. A A.y e. A (x e. y -> -. (F` y) = (F` x)) /\ A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y))))
73		r19.26-2 2221	. . . . . 6 |- (A.x e. A A.y e. A ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))) <-> (A.x e. A A.y e. A (x e. y -> -. (F` y) = (F` x)) /\ A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y))))
74	72, 73	sylibr 217	. . . . 5 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) -> A.x e. A A.y e. A ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))))
75	39, 74	syl 12	. . . 4 |- (A.x e. A A.y e. x -. (F` x) = (F` y) -> A.x e. A A.y e. A ((x e. y -> -. (F` y) = (F` x)) /\ (y e. x -> -. (F` x) = (F` y))))
76	31, 75	syl5 20	. . 3 |- (A C_ On -> (A.x e. A A.y e. x -. (F` x) = (F` y) -> A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)))
77	76	imdistani 491	. 2 |- ((A C_ On /\ A.x e. A A.y e. x -. (F` x) = (F` y)) -> (A C_ On /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)))
78		dff13 4850	. . . . . 6 |- ((F |` A):A-1-1->_V <-> ((F |` A):A-->_V /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)))
79		df-f1 4011	. . . . . 6 |- ((F |` A):A-1-1->_V <-> ((F |` A):A-->_V /\ Fun `'(F |` A)))
80	78, 79	bitr3i 192	. . . . 5 |- (((F |` A):A-->_V /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)) <-> ((F |` A):A-->_V /\ Fun `'(F |` A)))
81	80	simprbi 353	. . . 4 |- (((F |` A):A-->_V /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)) -> Fun `'(F |` A))
82		dffn2 4563	. . . 4 |- ((F |` A) Fn A <-> (F |` A):A-->_V)
83	81, 82	sylanb 498	. . 3 |- (((F |` A) Fn A /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)) -> Fun `'(F |` A))
84		tz7.48.1	. . . 4 |- F Fn On
85		fnssres 4526	. . . 4 |- ((F Fn On /\ A C_ On) -> (F |` A) Fn A)
86	84, 85	mpan 759	. . 3 |- (A C_ On -> (F |` A) Fn A)
87	83, 86	sylan 497	. 2 |- ((A C_ On /\ A.x e. A A.y e. A (((F |` A)` x) = ((F |` A)` y) -> x = y)) -> Fun `'(F |` A))
88	77, 87	syl 12	1 |- ((A C_ On /\ A.x e. A A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593  Ord word 3656  Oncon0 3657  `'ccnv 3985   |` cres 3988  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  ` cfv 3998

This theorem is referenced by:  tz7.48-2 5166  tz7.49 5168  abianfp 5171  ordtypelem4 5687  ordtypelem5 5688  zorn2lem4 5953  ordtypelem4OLD 15378  ordtypelem5OLD 15379

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-13 1311  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  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  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-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  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-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  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-f 4010  df-f1 4011  df-fv 4014

Copyright terms: Public domain