tz7.48lem

Description: A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997)

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

Proof

Step	Hyp	Ref	Expression
1		tz7.48.1	\|- F Fn On
2		r2al	\|- ( A. x e. A A. y e. x -. ( F ` x ) = ( F ` y ) <-> A. x A. y ( ( x e. A /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) )
3		simpl	\|- ( ( x e. A /\ y e. A ) -> x e. A )
4	3	anim1i	\|- ( ( ( x e. A /\ y e. A ) /\ y e. x ) -> ( x e. A /\ y e. x ) )
5	4	imim1i	\|- ( ( ( x e. A /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) -> ( ( ( x e. A /\ y e. A ) /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) )
6	5	expd	\|- ( ( ( x e. A /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) -> ( ( x e. A /\ y e. A ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) )
7	6	2alimi	\|- ( A. x A. y ( ( x e. A /\ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) -> A. x A. y ( ( x e. A /\ y e. A ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) )
8	2 7	sylbi	\|- ( A. x e. A A. y e. x -. ( F ` x ) = ( F ` y ) -> A. x A. y ( ( x e. A /\ y e. A ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) )
9		r2al	\|- ( A. x e. A A. y e. A ( y e. x -> -. ( F ` x ) = ( F ` y ) ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) )
10	8 9	sylibr	\|- ( 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 ) ) )
11		elequ1	\|- ( y = w -> ( y e. x <-> w e. x ) )
12		fveq2	\|- ( y = w -> ( F ` y ) = ( F ` w ) )
13	12	eqeq2d	\|- ( y = w -> ( ( F ` x ) = ( F ` y ) <-> ( F ` x ) = ( F ` w ) ) )
14	13	notbid	\|- ( y = w -> ( -. ( F ` x ) = ( F ` y ) <-> -. ( F ` x ) = ( F ` w ) ) )
15	11 14	imbi12d	\|- ( y = w -> ( ( y e. x -> -. ( F ` x ) = ( F ` y ) ) <-> ( w e. x -> -. ( F ` x ) = ( F ` w ) ) ) )
16	15	cbvralvw	\|- ( A. y e. A ( y e. x -> -. ( F ` x ) = ( F ` y ) ) <-> A. w e. A ( w e. x -> -. ( F ` x ) = ( F ` w ) ) )
17	16	ralbii	\|- ( 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 ) ) )
18		elequ2	\|- ( x = z -> ( w e. x <-> w e. z ) )
19		fveqeq2	\|- ( x = z -> ( ( F ` x ) = ( F ` w ) <-> ( F ` z ) = ( F ` w ) ) )
20	19	notbid	\|- ( x = z -> ( -. ( F ` x ) = ( F ` w ) <-> -. ( F ` z ) = ( F ` w ) ) )
21	18 20	imbi12d	\|- ( x = z -> ( ( w e. x -> -. ( F ` x ) = ( F ` w ) ) <-> ( w e. z -> -. ( F ` z ) = ( F ` w ) ) ) )
22	21	ralbidv	\|- ( x = z -> ( A. w e. A ( w e. x -> -. ( F ` x ) = ( F ` w ) ) <-> A. w e. A ( w e. z -> -. ( F ` z ) = ( F ` w ) ) ) )
23	22	cbvralvw	\|- ( 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 ) ) )
24		elequ1	\|- ( w = x -> ( w e. z <-> x e. z ) )
25		fveq2	\|- ( w = x -> ( F ` w ) = ( F ` x ) )
26	25	eqeq2d	\|- ( w = x -> ( ( F ` z ) = ( F ` w ) <-> ( F ` z ) = ( F ` x ) ) )
27	26	notbid	\|- ( w = x -> ( -. ( F ` z ) = ( F ` w ) <-> -. ( F ` z ) = ( F ` x ) ) )
28	24 27	imbi12d	\|- ( w = x -> ( ( w e. z -> -. ( F ` z ) = ( F ` w ) ) <-> ( x e. z -> -. ( F ` z ) = ( F ` x ) ) ) )
29	28	cbvralvw	\|- ( A. w e. A ( w e. z -> -. ( F ` z ) = ( F ` w ) ) <-> A. x e. A ( x e. z -> -. ( F ` z ) = ( F ` x ) ) )
30	29	ralbii	\|- ( 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 ) ) )
31		elequ2	\|- ( z = y -> ( x e. z <-> x e. y ) )
32		fveqeq2	\|- ( z = y -> ( ( F ` z ) = ( F ` x ) <-> ( F ` y ) = ( F ` x ) ) )
33	32	notbid	\|- ( z = y -> ( -. ( F ` z ) = ( F ` x ) <-> -. ( F ` y ) = ( F ` x ) ) )
34	31 33	imbi12d	\|- ( z = y -> ( ( x e. z -> -. ( F ` z ) = ( F ` x ) ) <-> ( x e. y -> -. ( F ` y ) = ( F ` x ) ) ) )
35	34	ralbidv	\|- ( z = y -> ( A. x e. A ( x e. z -> -. ( F ` z ) = ( F ` x ) ) <-> A. x e. A ( x e. y -> -. ( F ` y ) = ( F ` x ) ) ) )
36	35	cbvralvw	\|- ( 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 ) ) )
37	30 36	bitri	\|- ( 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 ) ) )
38	17 23 37	3bitri	\|- ( 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 ) ) )
39		ralcom	\|- ( 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 ) ) )
40	39	biimpi	\|- ( 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 ) ) )
41	38 40	sylbi	\|- ( 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 ) ) )
42	41	ancri	\|- ( 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 ) ) ) )
43		r19.26-2	\|- ( 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 ) ) ) )
44	42 43	sylibr	\|- ( 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 ) ) ) )
45	10 44	syl	\|- ( 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 ) ) ) )
46		fvres	\|- ( x e. A -> ( ( F \|` A ) ` x ) = ( F ` x ) )
47		fvres	\|- ( y e. A -> ( ( F \|` A ) ` y ) = ( F ` y ) )
48	46 47	eqeqan12d	\|- ( ( x e. A /\ y e. A ) -> ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) <-> ( F ` x ) = ( F ` y ) ) )
49	48	ad2antrl	\|- ( ( 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 ) ) )
50		ssel	\|- ( A C_ On -> ( x e. A -> x e. On ) )
51		ssel	\|- ( A C_ On -> ( y e. A -> y e. On ) )
52	50 51	anim12d	\|- ( A C_ On -> ( ( x e. A /\ y e. A ) -> ( x e. On /\ y e. On ) ) )
53		pm3.48	\|- ( ( ( 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 ) ) ) )
54		oridm	\|- ( ( -. ( F ` x ) = ( F ` y ) \/ -. ( F ` x ) = ( F ` y ) ) <-> -. ( F ` x ) = ( F ` y ) )
55		eqcom	\|- ( ( F ` x ) = ( F ` y ) <-> ( F ` y ) = ( F ` x ) )
56	55	notbii	\|- ( -. ( F ` x ) = ( F ` y ) <-> -. ( F ` y ) = ( F ` x ) )
57	56	orbi1i	\|- ( ( -. ( F ` x ) = ( F ` y ) \/ -. ( F ` x ) = ( F ` y ) ) <-> ( -. ( F ` y ) = ( F ` x ) \/ -. ( F ` x ) = ( F ` y ) ) )
58	54 57	bitr3i	\|- ( -. ( F ` x ) = ( F ` y ) <-> ( -. ( F ` y ) = ( F ` x ) \/ -. ( F ` x ) = ( F ` y ) ) )
59	53 58	syl6ibr	\|- ( ( ( x e. y -> -. ( F ` y ) = ( F ` x ) ) /\ ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) -> ( ( x e. y \/ y e. x ) -> -. ( F ` x ) = ( F ` y ) ) )
60	59	con2d	\|- ( ( ( x e. y -> -. ( F ` y ) = ( F ` x ) ) /\ ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) -> ( ( F ` x ) = ( F ` y ) -> -. ( x e. y \/ y e. x ) ) )
61		eloni	\|- ( x e. On -> Ord x )
62		eloni	\|- ( y e. On -> Ord y )
63		ordtri3	\|- ( ( Ord x /\ Ord y ) -> ( x = y <-> -. ( x e. y \/ y e. x ) ) )
64	63	biimprd	\|- ( ( Ord x /\ Ord y ) -> ( -. ( x e. y \/ y e. x ) -> x = y ) )
65	61 62 64	syl2an	\|- ( ( x e. On /\ y e. On ) -> ( -. ( x e. y \/ y e. x ) -> x = y ) )
66	60 65	syl9r	\|- ( ( 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 ) ) )
67	52 66	syl6	\|- ( 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 ) ) ) )
68	67	imp32	\|- ( ( 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 ) )
69	49 68	sylbid	\|- ( ( 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 ) )
70	69	exp32	\|- ( 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 ) ) ) )
71	70	a2d	\|- ( 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 ) ) ) )
72	71	2alimdv	\|- ( A C_ On -> ( A. x A. y ( ( x e. A /\ y e. A ) -> ( ( x e. y -> -. ( F ` y ) = ( F ` x ) ) /\ ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) -> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) ) ) )
73		r2al	\|- ( A. x e. A A. y e. A ( ( x e. y -> -. ( F ` y ) = ( F ` x ) ) /\ ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( x e. y -> -. ( F ` y ) = ( F ` x ) ) /\ ( y e. x -> -. ( F ` x ) = ( F ` y ) ) ) ) )
74		r2al	\|- ( A. x e. A A. y e. A ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) ) )
75	72 73 74	3imtr4g	\|- ( 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 ) ) )
76	45 75	syl5	\|- ( 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	\|- ( ( 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		fnssres	\|- ( ( F Fn On /\ A C_ On ) -> ( F \|` A ) Fn A )
79	1 78	mpan	\|- ( A C_ On -> ( F \|` A ) Fn A )
80		dffn2	\|- ( ( F \|` A ) Fn A <-> ( F \|` A ) : A --> _V )
81		dff13	\|- ( ( 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 ) ) )
82		df-f1	\|- ( ( F \|` A ) : A -1-1-> _V <-> ( ( F \|` A ) : A --> _V /\ Fun `' ( F \|` A ) ) )
83	81 82	bitr3i	\|- ( ( ( 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 ) ) )
84	83	simprbi	\|- ( ( ( F \|` A ) : A --> _V /\ A. x e. A A. y e. A ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) ) -> Fun `' ( F \|` A ) )
85	80 84	sylanb	\|- ( ( ( F \|` A ) Fn A /\ A. x e. A A. y e. A ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) ) -> Fun `' ( F \|` A ) )
86	79 85	sylan	\|- ( ( A C_ On /\ A. x e. A A. y e. A ( ( ( F \|` A ) ` x ) = ( ( F \|` A ) ` y ) -> x = y ) ) -> Fun `' ( F \|` A ) )
87	77 86	syl	\|- ( ( A C_ On /\ A. x e. A A. y e. x -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F \|` A ) )

Metamath Proof Explorer

Theorem tz7.48lem

Proof