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

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 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) ∈ V )

Proof

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