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

Metamath Proof Explorer

Theorem eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

Ref Expression
Assertion eldm3 ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ dom 𝐵 → 𝐴 ∈ V )
2 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3 reseq2 ⊢ ( { 𝐴 } = ∅ → ( 𝐵 ↾ { 𝐴 } ) = ( 𝐵 ↾ ∅ ) )
4 res0 ⊢ ( 𝐵 ↾ ∅ ) = ∅
5 3 4 eqtrdi ⊢ ( { 𝐴 } = ∅ → ( 𝐵 ↾ { 𝐴 } ) = ∅ )
6 2 5 sylbi ⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ↾ { 𝐴 } ) = ∅ )
7 6 necon1ai ⊢ ( ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ → 𝐴 ∈ V )
8 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝐵 ↔ 𝐴 ∈ dom 𝐵 ) )
9 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
10 9 reseq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ↾ { 𝑥 } ) = ( 𝐵 ↾ { 𝐴 } ) )
11 10 neeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ ) )
12 dfclel ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
13 12 exbii ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
14 vex ⊢ 𝑥 ∈ V
15 14 eldm2 ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
16 n0 ⊢ ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) )
17 elres ⊢ ( 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑧 ∈ { 𝑥 } ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
18 eleq1 ⊢ ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ → ( 𝑝 ∈ 𝐵 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
19 18 pm5.32i ⊢ ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
20 opeq1 ⊢ ( 𝑧 = 𝑥 → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
21 20 eqeq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
22 21 anbi1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
23 19 22 bitr3id ⊢ ( 𝑧 = 𝑥 → ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
24 23 exbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
25 14 24 rexsn ⊢ ( ∃ 𝑧 ∈ { 𝑥 } ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
26 17 25 bitri ⊢ ( 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
27 26 exbii ⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑝 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
28 excom ⊢ ( ∃ 𝑝 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
29 16 27 28 3bitri ⊢ ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
30 13 15 29 3bitr4i ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ )
31 8 11 30 vtoclbg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ ) )
32 1 7 31 pm5.21nii ⊢ ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ )