Metamath Proof Explorer

Theorem strfv2d

Description: Deduction version of strfv2 . (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses strfv2d.e ⊢ E = Slot E ⁡ ndx
strfv2d.s ⊢ φ → S ∈ V
strfv2d.f ⊢ φ → Fun ⁡ S -1 -1
strfv2d.n ⊢ φ → E ⁡ ndx C ∈ S
strfv2d.c ⊢ φ → C ∈ W
Assertion strfv2d ⊢ φ → C = E ⁡ S

Proof

Step Hyp Ref Expression
1 strfv2d.e ⊢ E = Slot E ⁡ ndx
2 strfv2d.s ⊢ φ → S ∈ V
3 strfv2d.f ⊢ φ → Fun ⁡ S -1 -1
4 strfv2d.n ⊢ φ → E ⁡ ndx C ∈ S
5 strfv2d.c ⊢ φ → C ∈ W
6 1 2 strfvnd ⊢ φ → E ⁡ S = S ⁡ E ⁡ ndx
7 cnvcnv2 ⊢ S -1 -1 = S ↾ V
8 7 fveq1i ⊢ S -1 -1 ⁡ E ⁡ ndx = S ↾ V ⁡ E ⁡ ndx
9 fvex ⊢ E ⁡ ndx ∈ V
10 fvres ⊢ E ⁡ ndx ∈ V → S ↾ V ⁡ E ⁡ ndx = S ⁡ E ⁡ ndx
11 9 10 ax-mp ⊢ S ↾ V ⁡ E ⁡ ndx = S ⁡ E ⁡ ndx
12 8 11 eqtri ⊢ S -1 -1 ⁡ E ⁡ ndx = S ⁡ E ⁡ ndx
13 5 elexd ⊢ φ → C ∈ V
14 opelxpi ⊢ E ⁡ ndx ∈ V ∧ C ∈ V → E ⁡ ndx C ∈ V × V
15 9 13 14 sylancr ⊢ φ → E ⁡ ndx C ∈ V × V
16 4 15 elind ⊢ φ → E ⁡ ndx C ∈ S ∩ V × V
17 cnvcnv ⊢ S -1 -1 = S ∩ V × V
18 16 17 eleqtrrdi ⊢ φ → E ⁡ ndx C ∈ S -1 -1
19 funopfv ⊢ Fun ⁡ S -1 -1 → E ⁡ ndx C ∈ S -1 -1 → S -1 -1 ⁡ E ⁡ ndx = C
20 3 18 19 sylc ⊢ φ → S -1 -1 ⁡ E ⁡ ndx = C
21 12 20 eqtr3id ⊢ φ → S ⁡ E ⁡ ndx = C
22 6 21 eqtr2d ⊢ φ → C = E ⁡ S