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

Metamath Proof Explorer

Theorem elbasfv

Description: Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015)

Ref Expression
Hypotheses elbasfv.s ⊢ S = F ⁡ Z
elbasfv.b ⊢ B = Base S
Assertion elbasfv ⊢ X ∈ B → Z ∈ V

Proof

Step Hyp Ref Expression
1 elbasfv.s ⊢ S = F ⁡ Z
2 elbasfv.b ⊢ B = Base S
3 n0i ⊢ X ∈ B → ¬ B = ∅
4 fvprc ⊢ ¬ Z ∈ V → F ⁡ Z = ∅
5 1 4 eqtrid ⊢ ¬ Z ∈ V → S = ∅
6 5 fveq2d ⊢ ¬ Z ∈ V → Base S = Base ∅
7 base0 ⊢ ∅ = Base ∅
8 6 2 7 3eqtr4g ⊢ ¬ Z ∈ V → B = ∅
9 3 8 nsyl2 ⊢ X ∈ B → Z ∈ V