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