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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 )
2 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
3 2 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
4 1 3 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 )
5 prid2g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
6 5 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
7 1 6 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
8 ffn ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 → 𝐹 Fn { 𝐴 , 𝐵 } )
9 8 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → 𝐹 Fn { 𝐴 , 𝐵 } )
10 fnpr2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
12 9 11 mpbid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
13 4 7 12 3jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
14 10 biimpar ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → 𝐹 Fn { 𝐴 , 𝐵 } )
15 14 3ad2antr3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐹 Fn { 𝐴 , 𝐵 } )
16 simpr3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
17 2 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
18 simpr1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 )
19 17 18 opelxpd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ ( { 𝐴 , 𝐵 } × 𝐶 ) )
20 5 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
21 simpr2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
22 20 21 opelxpd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( { 𝐴 , 𝐵 } × 𝐶 ) )
23 19 22 prssd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ⊆ ( { 𝐴 , 𝐵 } × 𝐶 ) )
24 16 23 eqsstrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐹 ⊆ ( { 𝐴 , 𝐵 } × 𝐶 ) )
25 dff2 ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ↔ ( 𝐹 Fn { 𝐴 , 𝐵 } ∧ 𝐹 ⊆ ( { 𝐴 , 𝐵 } × 𝐶 ) ) )
26 15 24 25 sylanbrc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) → 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 )
27 13 26 impbida ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝐶 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) )