tz7.48lem

Description: A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997) Extract onelfvnef1 . (Proof shortened by Matthew House, 6-Sep-2026)

		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		dffn2	$⊢ F Fn On \leftrightarrow F : On ⟶ V$
3	1 2	mpbi	$⊢ F : On ⟶ V$
4		fssres	$⊢ (F : On ⟶ V \land A \subseteq On) \to ({F ↾}_{A}) : A ⟶ V$
5	3 4	mpan	$⊢ A \subseteq On \to ({F ↾}_{A}) : A ⟶ V$
6		fvres	$⊢ x \in A \to ({F ↾}_{A}) (x) = F (x)$
7		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
8	6 7	eqeqan12d	$⊢ (x \in A \land y \in A) \to (({F ↾}_{A}) (x) = ({F ↾}_{A}) (y) \leftrightarrow F (x) = F (y))$
9	8	necon3abid	$⊢ (x \in A \land y \in A) \to (({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y) \leftrightarrow \neg F (x) = F (y))$
10	9	imbi2d	$⊢ (x \in A \land y \in A) \to ((y \in x \to ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y)) \leftrightarrow (y \in x \to \neg F (x) = F (y)))$
11	10	exbiri	$⊢ x \in A \to (y \in A \to ((y \in x \to \neg F (x) = F (y)) \to (y \in x \to ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y))))$
12	11	com23	$⊢ x \in A \to ((y \in x \to \neg F (x) = F (y)) \to (y \in A \to (y \in x \to ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y))))$
13	12	ralimdv2	$⊢ x \in A \to (\forall y \in x \neg F (x) = F (y) \to \forall y \in A (y \in x \to ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y)))$
14	13	ralimia	$⊢ \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 ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y))$
15		onelfvnef1	$⊢ (({F ↾}_{A}) : A ⟶ V \land A \subseteq On \land \forall x \in A \forall y \in A (y \in x \to ({F ↾}_{A}) (x) \neq ({F ↾}_{A}) (y))) \to ({F ↾}_{A}) : A \underset{1-1}{⟶} V$
16	14 15	syl3an3	$⊢ (({F ↾}_{A}) : A ⟶ V \land A \subseteq On \land \forall x \in A \forall y \in x \neg F (x) = F (y)) \to ({F ↾}_{A}) : A \underset{1-1}{⟶} V$
17	5 16	syl3an1	$⊢ (A \subseteq On \land A \subseteq On \land \forall x \in A \forall y \in x \neg F (x) = F (y)) \to ({F ↾}_{A}) : A \underset{1-1}{⟶} V$
18	17	3anidm12	$⊢ (A \subseteq On \land \forall x \in A \forall y \in x \neg F (x) = F (y)) \to ({F ↾}_{A}) : A \underset{1-1}{⟶} V$
19		df-f1	$⊢ ({F ↾}_{A}) : A \underset{1-1}{⟶} V \leftrightarrow (({F ↾}_{A}) : A ⟶ V \land Fun {({F ↾}_{A})}^{-1})$
20	19	simprbi	$⊢ ({F ↾}_{A}) : A \underset{1-1}{⟶} V \to Fun {({F ↾}_{A})}^{-1}$
21	18 20	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