Metamath Proof Explorer

Theorem fpr2g

Description: A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Assertion fpr2g ⊢A∈V∧B∈W→F:AB⟶C↔F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B

Proof

Step Hyp Ref Expression
1 simpr ⊢A∈V∧B∈W∧F:AB⟶C→F:AB⟶C
2 prid1g ⊢A∈V→A∈AB
3 2 ad2antrr ⊢A∈V∧B∈W∧F:AB⟶C→A∈AB
4 1 3 ffvelcdmd ⊢A∈V∧B∈W∧F:AB⟶C→F⁡A∈C
5 prid2g ⊢B∈W→B∈AB
6 5 ad2antlr ⊢A∈V∧B∈W∧F:AB⟶C→B∈AB
7 1 6 ffvelcdmd ⊢A∈V∧B∈W∧F:AB⟶C→F⁡B∈C
8 ffn ⊢F:AB⟶C→FFnAB
9 8 adantl ⊢A∈V∧B∈W∧F:AB⟶C→FFnAB
10 fnpr2g ⊢A∈V∧B∈W→FFnAB↔F=AF⁡ABF⁡B
11 10 adantr ⊢A∈V∧B∈W∧F:AB⟶C→FFnAB↔F=AF⁡ABF⁡B
12 9 11 mpbid ⊢A∈V∧B∈W∧F:AB⟶C→F=AF⁡ABF⁡B
13 4 7 12 3jca ⊢A∈V∧B∈W∧F:AB⟶C→F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B
14 10 biimpar ⊢A∈V∧B∈W∧F=AF⁡ABF⁡B→FFnAB
15 14 3ad2antr3 ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→FFnAB
16 simpr3 ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→F=AF⁡ABF⁡B
17 2 ad2antrr ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→A∈AB
18 simpr1 ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→F⁡A∈C
19 17 18 opelxpd ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→AF⁡A∈AB×C
20 5 ad2antlr ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→B∈AB
21 simpr2 ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→F⁡B∈C
22 20 21 opelxpd ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→BF⁡B∈AB×C
23 19 22 prssd ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→AF⁡ABF⁡B⊆AB×C
24 16 23 eqsstrd ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→F⊆AB×C
25 dff2 ⊢F:AB⟶C↔FFnAB∧F⊆AB×C
26 15 24 25 sylanbrc ⊢A∈V∧B∈W∧F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B→F:AB⟶C
27 13 26 impbida ⊢A∈V∧B∈W→F:AB⟶C↔F⁡A∈C∧F⁡B∈C∧F=AF⁡ABF⁡B