Theorem tz7.48lem 3946

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 (_ 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 3725	. . . . . . . . . . . 12 |- (x e. A -> ((F |` A)` x) = (F` x))
2		fvres 3725	. . . . . . . . . . . 12 |- (y e. A -> ((F |` A)` y) = (F` y))
3	1, 2	eqeqan12d 1487	. . . . . . . . . . 11 |- ((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) <-> (F` x) = (F` y)))
4	3	ad2antrl 406	. . . . . . . . . 10 |- ((A (_ 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 2059	. . . . . . . . . . . . 13 |- (A (_ On -> (x e. A -> x e. On))
6		ssel 2059	. . . . . . . . . . . . 13 |- (A (_ On -> (y e. A -> y e. On))
7	5, 6	anim12d 557	. . . . . . . . . . . 12 |- (A (_ On -> ((x e. A /\ y e. A) -> (x e. On /\ y e. On)))
8		pm3.48 556	. . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> -. (F` x) = (F` y))
10		eqcom 1474	. . . . . . . . . . . . . . . . . 18 |- ((F` x) = (F` y) <-> (F` y) = (F` x))
11	10	negbii 187	. . . . . . . . . . . . . . . . 17 |- (-. (F` x) = (F` y) <-> -. (F` y) = (F` x))
12	11	orbi1i 256	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
13	9, 12	bitr3 175	. . . . . . . . . . . . . . 15 |- (-. (F` x) = (F` y) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
14	8, 13	syl6ibr 213	. . . . . . . . . . . . . 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 91	. . . . . . . . . . . . 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 2978	. . . . . . . . . . . . . . 15 |- ((Ord x /\ Ord y) -> (x = y <-> -. (x e. y \/ y e. x)))
17	16	biimprd 154	. . . . . . . . . . . . . 14 |- ((Ord x /\ Ord y) -> (-. (x e. y \/ y e. x) -> x = y))
18		eloni 2953	. . . . . . . . . . . . . 14 |- (x e. On -> Ord x)
19		eloni 2953	. . . . . . . . . . . . . 14 |- (y e. On -> Ord y)
20	17, 18, 19	syl2an 454	. . . . . . . . . . . . 13 |- ((x e. On /\ y e. On) -> (-. (x e. y \/ y e. x) -> x = y))
21	15, 20	syl9r 58	. . . . . . . . . . . 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 22	. . . . . . . . . . 11 |- (A (_ 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 363	. . . . . . . . . 10 |- ((A (_ 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 203	. . . . . . . . 9 |- ((A (_ 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 377	. . . . . . . 8 |- (A (_ 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 13	. . . . . . 7 |- (A (_ 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	19.20dv 1287	. . . . . 6 |- (A (_ 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	19.20dv 1287	. . . . 5 |- (A (_ 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 1673	. . . . 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 1673	. . . . 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 552	. . . 4 |- (A (_ 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		pm3.26 319	. . . . . . . . . 10 |- ((x e. A /\ y e. A) -> x e. A)
33	32	anim1i 334	. . . . . . . . 9 |- (((x e. A /\ y e. A) /\ y e. x) -> (x e. A /\ y e. x))
34	33	imim1i 16	. . . . . . . 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 375	. . . . . . 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	19.20i2 991	. . . . . 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 1673	. . . . . 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 1673	. . . . . 6 |- (A.x e. A A.y e. A (y e. x -> -. (F` x) = (F` y)) <-> A.xA.y((x e. A /\