Metamath Proof Explorer

Theorem resfunexgALT

Description: Alternate proof of resfunexg , shorter but requiring ax-pow and ax-un . (Contributed by NM, 7-Apr-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion resfunexgALT ⊢ Fun ⁡ A ∧ B ∈ C → A ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 dmresexg ⊢ B ∈ C → dom ⁡ A ↾ B ∈ V
2 1 adantl ⊢ Fun ⁡ A ∧ B ∈ C → dom ⁡ A ↾ B ∈ V
3 df-ima ⊢ A B = ran ⁡ A ↾ B
4 funimaexg ⊢ Fun ⁡ A ∧ B ∈ C → A B ∈ V
5 3 4 eqeltrrid ⊢ Fun ⁡ A ∧ B ∈ C → ran ⁡ A ↾ B ∈ V
6 2 5 jca ⊢ Fun ⁡ A ∧ B ∈ C → dom ⁡ A ↾ B ∈ V ∧ ran ⁡ A ↾ B ∈ V
7 xpexg ⊢ dom ⁡ A ↾ B ∈ V ∧ ran ⁡ A ↾ B ∈ V → dom ⁡ A ↾ B × ran ⁡ A ↾ B ∈ V
8 relres ⊢ Rel ⁡ A ↾ B
9 relssdmrn ⊢ Rel ⁡ A ↾ B → A ↾ B ⊆ dom ⁡ A ↾ B × ran ⁡ A ↾ B
10 8 9 ax-mp ⊢ A ↾ B ⊆ dom ⁡ A ↾ B × ran ⁡ A ↾ B
11 ssexg ⊢ A ↾ B ⊆ dom ⁡ A ↾ B × ran ⁡ A ↾ B ∧ dom ⁡ A ↾ B × ran ⁡ A ↾ B ∈ V → A ↾ B ∈ V
12 10 11 mpan ⊢ dom ⁡ A ↾ B × ran ⁡ A ↾ B ∈ V → A ↾ B ∈ V
13 6 7 12 3syl ⊢ Fun ⁡ A ∧ B ∈ C → A ↾ B ∈ V