This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = (/) )