iresn0n0

Description: The identity function restricted to a class A is empty iff the class A is empty. (Contributed by AV, 30-Jan-2024)

		Ref	Expression
	Assertion	iresn0n0	$⊢ A = \emptyset \leftrightarrow {I ↾}_{A} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		opab0	$⊢ \{⟨x, y⟩ \| (x \in A \land y = x)\} = \emptyset \leftrightarrow \forall x \forall y \neg (x \in A \land y = x)$
2		opabresid	$⊢ {I ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land y = x)\}$
3	2	eqeq1i	$⊢ {I ↾}_{A} = \emptyset \leftrightarrow \{⟨x, y⟩ \| (x \in A \land y = x)\} = \emptyset$
4		nel02	$⊢ A = \emptyset \to \neg x \in A$
5	4	intnanrd	$⊢ A = \emptyset \to \neg (x \in A \land y = x)$
6	5	alrimivv	$⊢ A = \emptyset \to \forall x \forall y \neg (x \in A \land y = x)$
7		ianor	$⊢ \neg (x \in A \land y = x) \leftrightarrow (\neg x \in A \lor \neg y = x)$
8	7	albii	$⊢ \forall y \neg (x \in A \land y = x) \leftrightarrow \forall y (\neg x \in A \lor \neg y = x)$
9		19.32v	$⊢ \forall y (\neg x \in A \lor \neg y = x) \leftrightarrow (\neg x \in A \lor \forall y \neg y = x)$
10		id	$⊢ \neg x \in A \to \neg x \in A$
11		ax6v	$⊢ \neg \forall y \neg y = x$
12	11	pm2.21i	$⊢ \forall y \neg y = x \to \neg x \in A$
13	10 12	jaoi	$⊢ (\neg x \in A \lor \forall y \neg y = x) \to \neg x \in A$
14	9 13	sylbi	$⊢ \forall y (\neg x \in A \lor \neg y = x) \to \neg x \in A$
15	8 14	sylbi	$⊢ \forall y \neg (x \in A \land y = x) \to \neg x \in A$
16	15	alimi	$⊢ \forall x \forall y \neg (x \in A \land y = x) \to \forall x \neg x \in A$
17		eq0	$⊢ A = \emptyset \leftrightarrow \forall x \neg x \in A$
18	16 17	sylibr	$⊢ \forall x \forall y \neg (x \in A \land y = x) \to A = \emptyset$
19	6 18	impbii	$⊢ A = \emptyset \leftrightarrow \forall x \forall y \neg (x \in A \land y = x)$
20	1 3 19	3bitr4ri	$⊢ A = \emptyset \leftrightarrow {I ↾}_{A} = \emptyset$

Metamath Proof Explorer

Theorem iresn0n0

Proof