Metamath Proof Explorer

Theorem elpmg

Description: The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion elpmg ⊢A∈V∧B∈W→C∈A↑𝑝𝑚B↔Fun⁡C∧C⊆B×A

Proof

Step Hyp Ref Expression
1 pmvalg ⊢A∈V∧B∈W→A↑𝑝𝑚B=g∈𝒫B×A|Fun⁡g
2 1 eleq2d ⊢A∈V∧B∈W→C∈A↑𝑝𝑚B↔C∈g∈𝒫B×A|Fun⁡g
3 funeq ⊢g=C→Fun⁡g↔Fun⁡C
4 3 elrab ⊢C∈g∈𝒫B×A|Fun⁡g↔C∈𝒫B×A∧Fun⁡C
5 2 4 bitrdi ⊢A∈V∧B∈W→C∈A↑𝑝𝑚B↔C∈𝒫B×A∧Fun⁡C
6 5 biancomd ⊢A∈V∧B∈W→C∈A↑𝑝𝑚B↔Fun⁡C∧C∈𝒫B×A
7 elex ⊢C∈𝒫B×A→C∈V
8 7 a1i ⊢A∈V∧B∈W→C∈𝒫B×A→C∈V
9 xpexg ⊢B∈W∧A∈V→B×A∈V
10 9 ancoms ⊢A∈V∧B∈W→B×A∈V
11 ssexg ⊢C⊆B×A∧B×A∈V→C∈V
12 11 expcom ⊢B×A∈V→C⊆B×A→C∈V
13 10 12 syl ⊢A∈V∧B∈W→C⊆B×A→C∈V
14 elpwg ⊢C∈V→C∈𝒫B×A↔C⊆B×A
15 14 a1i ⊢A∈V∧B∈W→C∈V→C∈𝒫B×A↔C⊆B×A
16 8 13 15 pm5.21ndd ⊢A∈V∧B∈W→C∈𝒫B×A↔C⊆B×A
17 16 anbi2d ⊢A∈V∧B∈W→Fun⁡C∧C∈𝒫B×A↔Fun⁡C∧C⊆B×A
18 6 17 bitrd ⊢A∈V∧B∈W→C∈A↑𝑝𝑚B↔Fun⁡C∧C⊆B×A