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	⊢ ( 𝐴 = ∅ ↔ ( I ↾ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		opab0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) )
2		opabresid	⊢ ( I ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) }
3	2	eqeq1i	⊢ ( ( I ↾ 𝐴 ) = ∅ ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) } = ∅ )
4		nel02	⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 )
5	4	intnanrd	⊢ ( 𝐴 = ∅ → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) )
6	5	alrimivv	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) )
7		ianor	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 = 𝑥 ) )
8	7	albii	⊢ ( ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) ↔ ∀ 𝑦 ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 = 𝑥 ) )
9		19.32v	⊢ ( ∀ 𝑦 ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 = 𝑥 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ∀ 𝑦 ¬ 𝑦 = 𝑥 ) )
10		id	⊢ ( ¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴 )
11		ax6v	⊢ ¬ ∀ 𝑦 ¬ 𝑦 = 𝑥
12	11	pm2.21i	⊢ ( ∀ 𝑦 ¬ 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝐴 )
13	10 12	jaoi	⊢ ( ( ¬ 𝑥 ∈ 𝐴 ∨ ∀ 𝑦 ¬ 𝑦 = 𝑥 ) → ¬ 𝑥 ∈ 𝐴 )
14	9 13	sylbi	⊢ ( ∀ 𝑦 ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 = 𝑥 ) → ¬ 𝑥 ∈ 𝐴 )
15	8 14	sylbi	⊢ ( ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) → ¬ 𝑥 ∈ 𝐴 )
16	15	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) → ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
17		eq0	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
18	16 17	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) → 𝐴 = ∅ )
19	6 18	impbii	⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥 ) )
20	1 3 19	3bitr4ri	⊢ ( 𝐴 = ∅ ↔ ( I ↾ 𝐴 ) = ∅ )