Theorem tz7.48lem 2993

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 group(s):   x,y,F   x,A,y

Proof of Theorem tz7.48lem

Step	Hyp	Ref	Expression
1		fvres 2840	. . . . . . . . . . . 12 |- (x e. A -> ((F |` A)` x) = (F` x))
2		fvres 2840	. . . . . . . . . . . 12 |- (y e. A -> ((F |` A)` y) = (F` y))
3	1, 2	cleqan12d 1116	. . . . . . . . . . 11 |- ((x e. A /\ y e. A) -> (((F |` A)` x) = ((F |` A)` y) <-> (F` x) = (F` y)))
4	3	ad2antrl 322	. . . . . . . . . 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 1502	. . . . . . . . . . . . 13 |- (A (_ On -> (x e. A -> x e. On))
6		ssel 1502	. . . . . . . . . . . . 13 |- (A (_ On -> (y e. A -> y e. On))
7	5, 6	anim12d 431	. . . . . . . . . . . 12 |- (A (_ On -> ((x e. A /\ y e. A) -> (x e. On /\ y e. On)))
8		pm3.48 430	. . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> -. (F` x) = (F` y))
10		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 |- ((F` x) = (F` y) <-> (F` y) = (F` x))
11	10	negbii 162	. . . . . . . . . . . . . . . . 17 |- (-. (F` x) = (F` y) <-> -. (F` y) = (F` x))
12	11	orbi1i 215	. . . . . . . . . . . . . . . 16 |- ((-. (F` x) = (F` y) \/ -. (F` x) = (F` y)) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
13	9, 12	bitr3 153	. . . . . . . . . . . . . . 15 |- (-. (F` x) = (F` y) <-> (-. (F` y) = (F` x) \/ -. (F` x) = (F` y)))
14	8, 13	syl6ibr 186	. . . . . . . . . . . . . 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 83	. . . . . . . . . . . . 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 2234	. . . . . . . . . . . . . . 15 |- ((Ord x /\ Ord y) -> (x = y <-> -. (x e. y \/ y e. x)))
17	16	biimprd 136	. . . . . . . . . . . . . 14 |- ((Ord x /\ Ord y) -> (-. (x e. y \/ y e. x) -> x = y))
18		eloni 2209	. . . . . . . . . . . . . 14 |- (x e. On -> Ord x)
19		eloni 2209	. . . . . . . . . . . . . 14 |- (y e. On -> Ord y)
20	17, 18, 19	syl2an 349	. . . . . . . . . . . . 13 |- ((x e. On /\ y e. On) -> (-. (x e. y \/ y e. x) -> x = y))
21	15, 20	syl9r 56	. . . . . . . . . . . 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 23	. . . . . . . . . . 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 281	. . . . . . . . . 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 178	. . . . . . . . 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 294	. . . . . . . 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 15	. . . . . . 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 946	. . . . . 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 946	. . . . 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 1231	. . . . 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 1231	. . . . 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 426	. . . 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 256	. . . . . . . . . . 11 |- ((x e. A /\ y e. A) -> x e. A)
33	32	anim1i 269	. . . . . . . . . 10 |- (((x e. A /\ y e. A) /\ y e. x) -> (x e. A /\ y e. x))
34	33	syl4 19	. . . . . . . . 9 |- (((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 292	. . . . . . . 8 |- (((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.20i 691	. . . . . . 7 |- (A.y((x e. A /\ y e. x) -> -. (F` x) = (F` y)) -> A.y((x e. A /\ y e. A) -> (y e. x -> -. (F` x) = (F` y))))
37	36	19.20i 691	. . . . . 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))))
38		r2al 1231	. . . . . 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)))
39		r2al 1231	. . . . . 6 |- (A.x e. A A.y e. A (y e. x ->