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