Theorem 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 = (/) <-> ( _I |` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		opab0	|- ( { <. x , y >. | ( x e. A /\ y = x ) } = (/) <-> A. x A. y -. ( x e. A /\ y = x ) )
2		opabresid	|- ( _I |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }
3	2	eqeq1i	|- ( ( _I |` A ) = (/) <-> { <. x , y >. | ( x e. A /\ y = x ) } = (/) )
4		nel02	|- ( A = (/) -> -. x e. A )
5	4	intnanrd	|- ( A = (/) -> -. ( x e. A /\ y = x ) )
6	5	alrimivv	|- ( A = (/) -> A. x A. y -. ( x e. A /\ y = x ) )
7		ianor	|- ( -. ( x e. A /\ y = x ) <-> ( -. x e. A \/ -. y = x ) )
8	7	albii	|- ( A. y -. ( x e. A /\ y = x ) <-> A. y ( -. x e. A \/ -. y = x ) )
9		19.32v	|- ( A. y ( -. x e. A \/ -. y = x ) <-> ( -. x e. A \/ A. y -. y = x ) )
10		id	|- ( -. x e. A -> -. x e. A )
11		ax6v	|- -. A. y -. y = x
12	11	pm2.21i	|- ( A. y -. y = x -> -. x e. A )
13	10 12	jaoi	|- ( ( -. x e. A \/ A. y -. y = x ) -> -. x e. A )
14	9 13	sylbi	|- ( A. y ( -. x e. A \/ -. y = x ) -> -. x e. A )
15	8 14	sylbi	|- ( A. y -. ( x e. A /\ y = x ) -> -. x e. A )
16	15	alimi	|- ( A. x A. y -. ( x e. A /\ y = x ) -> A. x -. x e. A )
17		eq0	|- ( A = (/) <-> A. x -. x e. A )
18	16 17	sylibr	|- ( A. x A. y -. ( x e. A /\ y = x ) -> A = (/) )
19	6 18	impbii	|- ( A = (/) <-> A. x A. y -. ( x e. A /\ y = x ) )
20	1 3 19	3bitr4ri	|- ( A = (/) <-> ( _I |` A ) = (/) )