Theorem 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	$$⊢FFn\mathrm{On}$$
Assertion	tz7.48lem	$$⊢\left(A\subseteq \mathrm{On}\wedge \forall x\in A\forall y\in x\neg F\left(x\right)=F\left(y\right)\right)\to \mathrm{Fun}{\left({F\upharpoonright }_A\right)}^{-1}$$

Proof

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