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

Metamath Proof Explorer

Theorem divsfval

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

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

Proof

Step Hyp Ref Expression
1 ercpbl.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
2 ercpbl.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 eqtrid ⊢ ( 𝜑 → dom 𝐹 = 𝑉 )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ 𝑉 ) )
18 17 notbid ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ dom 𝐹 ↔ ¬ 𝐴 ∈ 𝑉 ) )
19 ndmfv ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
20 18 19 biimtrrdi ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
21 ecdmn0 ⊢ ( 𝐴 ∈ dom ∼ ↔ [ 𝐴 ] ∼ ≠ ∅ )
22 erdm ⊢ ( ∼ Er 𝑉 → dom ∼ = 𝑉 )
23 1 22 syl ⊢ ( 𝜑 → dom ∼ = 𝑉 )
24 23 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ dom ∼ ↔ 𝐴 ∈ 𝑉 ) )
25 24 biimpd ⊢ ( 𝜑 → ( 𝐴 ∈ dom ∼ → 𝐴 ∈ 𝑉 ) )
26 21 25 biimtrrid ⊢ ( 𝜑 → ( [ 𝐴 ] ∼ ≠ ∅ → 𝐴 ∈ 𝑉 ) )
27 26 necon1bd ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → [ 𝐴 ] ∼ = ∅ ) )
28 20 27 jcad ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( ( 𝐹 ‘ 𝐴 ) = ∅ ∧ [ 𝐴 ] ∼ = ∅ ) ) )
29 eqtr3 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ∅ ∧ [ 𝐴 ] ∼ = ∅ ) → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )
30 28 29 syl6 ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ ) )
31 9 30 pm2.61d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ )