Theorem divsfval

Description: Value of the function in qusval . (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ V )
	ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
Assertion	divsfval	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
2		ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ V )
3		ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4	1	ecss	⊢ ( 𝜑 → [ 𝐴 ] ∼ ⊆ 𝑉 )
5	2 4	ssexd	⊢ ( 𝜑 → [ 𝐴 ] ∼ ∈ V )
6		eceq1	⊢ ( 𝑥 = 𝐴 → [ 𝑥 ] ∼ = [ 𝐴 ] ∼ )
7	6 3	fvmptg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ [ 𝐴 ] ∼ ∈ V ) → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )
8	5 7	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )
9	8	expcom	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ ) )
10	3	dmeqi	⊢ dom 𝐹 = dom ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
11	1	ecss	⊢ ( 𝜑 → [ 𝑥 ] ∼ ⊆ 𝑉 )
12	2 11	ssexd	⊢ ( 𝜑 → [ 𝑥 ] ∼ ∈ V )
13	12	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 [ 𝑥 ] ∼ ∈ V )
14		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑉 [ 𝑥 ] ∼ ∈ V → dom ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = 𝑉 )
15	13 14	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = 𝑉 )
16	10 15	syl5eq	⊢ ( 𝜑 → dom 𝐹 = 𝑉 )
17	16	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ 𝑉 ) )
18	17	notbid	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ dom 𝐹 ↔ ¬ 𝐴 ∈ 𝑉 ) )
19		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
20	18 19	syl6bir	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
21		ecdmn0	⊢ ( 𝐴 ∈ dom ∼ ↔ [ 𝐴 ] ∼ ≠ ∅ )
22		erdm	⊢ ( ∼ Er 𝑉 → dom ∼ = 𝑉 )
23	1 22	syl	⊢ ( 𝜑 → dom ∼ = 𝑉 )
24	23	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ dom ∼ ↔ 𝐴 ∈ 𝑉 ) )
25	24	biimpd	⊢ ( 𝜑 → ( 𝐴 ∈ dom ∼ → 𝐴 ∈ 𝑉 ) )
26	21 25	syl5bir	⊢ ( 𝜑 → ( [ 𝐴 ] ∼ ≠ ∅ → 𝐴 ∈ 𝑉 ) )
27	26	necon1bd	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → [ 𝐴 ] ∼ = ∅ ) )
28	20 27	jcad	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( ( 𝐹 ‘ 𝐴 ) = ∅ ∧ [ 𝐴 ] ∼ = ∅ ) ) )
29		eqtr3	⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ∅ ∧ [ 𝐴 ] ∼ = ∅ ) → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )
30	28 29	syl6	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ ) )
31	9 30	pm2.61d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )