strfv2d

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

	Ref	Expression
Hypotheses	strfv2d.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strfv2d.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	strfv2d.f	⊢ ( 𝜑 → Fun ^◡ ^◡ 𝑆 )
	strfv2d.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
	strfv2d.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	strfv2d	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strfv2d.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2		strfv2d.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		strfv2d.f	⊢ ( 𝜑 → Fun ^◡ ^◡ 𝑆 )
4		strfv2d.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
5		strfv2d.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6	1 2	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) )
7		cnvcnv2	⊢ ^◡ ^◡ 𝑆 = ( 𝑆 ↾ V )
8	7	fveq1i	⊢ ( ^◡ ^◡ 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = ( ( 𝑆 ↾ V ) ‘ ( 𝐸 ‘ ndx ) )
9		fvex	⊢ ( 𝐸 ‘ ndx ) ∈ V
10		fvres	⊢ ( ( 𝐸 ‘ ndx ) ∈ V → ( ( 𝑆 ↾ V ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) )
11	9 10	ax-mp	⊢ ( ( 𝑆 ↾ V ) ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) )
12	8 11	eqtri	⊢ ( ^◡ ^◡ 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) )
13	5	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
14		opelxpi	⊢ ( ( ( 𝐸 ‘ ndx ) ∈ V ∧ 𝐶 ∈ V ) → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
15	9 13 14	sylancr	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( V × V ) )
16	4 15	elind	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ( 𝑆 ∩ ( V × V ) ) )
17		cnvcnv	⊢ ^◡ ^◡ 𝑆 = ( 𝑆 ∩ ( V × V ) )
18	16 17	eleqtrrdi	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ^◡ ^◡ 𝑆 )
19		funopfv	⊢ ( Fun ^◡ ^◡ 𝑆 → ( ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ ^◡ ^◡ 𝑆 → ( ^◡ ^◡ 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 ) )
20	3 18 19	sylc	⊢ ( 𝜑 → ( ^◡ ^◡ 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
21	12 20	eqtr3id	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
22	6 21	eqtr2d	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )

Metamath Proof Explorer

Theorem strfv2d

Proof