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		ralcom	$⊢ \forall y \in A \forall x \in A (x \in y \to \neg F (y) = F (x)) \leftrightarrow \forall x \in A \forall y \in A (x \in y \to \neg F (y) = F (x))$
40	39	biimpi	$⊢ \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))$
41	38 40	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))$
42	41	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)))$
43		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)))$
44	42 43	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)))$
45	10 44	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)))$
46		fvres	$⊢ x \in A \to ({F ↾}_{A}) (x) = F (x)$
47		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
48	46 47	eqeqan12d	$⊢ (x \in A \land y \in A) \to (({F ↾}_{A}) (x) = ({F ↾}_{A}) (y) \leftrightarrow F (x) = F (y))$
49	48	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))$
50		ssel	$⊢ A \subseteq On \to (x \in A \to x \in On)$
51		ssel	$⊢ A \subseteq On \to (y \in A \to y \in On)$
52	50 51	anim12d	$⊢ A \subseteq On \to ((x \in A \land y \in A) \to (x \in On \land y \in On))$
53		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)))$
54		oridm	$⊢ (\neg F (x) = F (y) \lor \neg F (x) = F (y)) \leftrightarrow \neg F (x) = F (y)$
55		eqcom	$⊢ F (x) = F (y) \leftrightarrow F (y) = F (x)$
56	55	notbii	$⊢ \neg F (x) = F (y) \leftrightarrow \neg F (y) = F (x)$
57	56	orbi1i	$⊢ (\neg F (x) = F (y) \lor \neg F (x) = F (y)) \leftrightarrow (\neg F (y) = F (x) \lor \neg F (x) = F (y))$
58	54 57	bitr3i	$⊢ \neg F (x) = F (y) \leftrightarrow (\neg F (y) = F (x) \lor \neg F (x) = F (y))$
59	53 58	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))$
60	59	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))$
61		eloni	$⊢ x \in On \to Ord x$
62		eloni	$⊢ y \in On \to Ord y$
63		ordtri3	$⊢ (Ord x \land Ord y) \to (x = y \leftrightarrow \neg (x \in y \lor y \in x))$
64	63	biimprd	$⊢ (Ord x \land Ord y) \to (\neg (x \in y \lor y \in x) \to x = y)$
65	61 62 64	syl2an	$⊢ (x \in On \land y \in On) \to (\neg (x \in y \lor y \in x) \to x = y)$
66	60 65	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))$
67	52 66	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)))$
68	67	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)$
69	49 68	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)$
70	69	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)))$
71	70	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)))$
72	71	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)))$
73		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))))$
74		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))$
75	72 73 74	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))$
76	45 75	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))$
77	76	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))$
78		fnssres	$⊢ (F Fn On \land A \subseteq On) \to ({F ↾}_{A}) Fn A$
79	1 78	mpan	$⊢ A \subseteq On \to ({F ↾}_{A}) Fn A$
80		dffn2	$⊢ ({F ↾}_{A}) Fn A \leftrightarrow ({F ↾}_{A}) : A ⟶ V$
81		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))$
82		df-f1	$⊢ ({F ↾}_{A}) : A \underset{1-1}{⟶} V \leftrightarrow (({F ↾}_{A}) : A ⟶ V \land Fun {({F ↾}_{A})}^{-1})$
83	81 82	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})$
84	83	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}$
85	80 84	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}$
86	79 85	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}$
87	77 86	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