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 \subseteq On \land \forall x \in A \forall y \in x \neg F (x) = F (y)) \to Fun {({F ↾}_{A})}^{-1}$

Proof

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

Metamath Proof Explorer

Theorem tz7.48lem

Proof