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 : A B ⟶ C ↔ F ⁡ A ∈ C ∧ F ⁡ B ∈ C ∧ F = A F ⁡ A B F ⁡ B

Proof

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