Metamath Proof Explorer

Theorem fprb

Description: A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013)

Ref Expression
Hypotheses fprb.1 ⊢ 𝐴 ∈ V
fprb.2 ⊢ 𝐵 ∈ V
Assertion fprb ( 𝐴 ≠ 𝐵 → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 fprb.1 ⊢ 𝐴 ∈ V
2 fprb.2 ⊢ 𝐵 ∈ V
3 1 prid1 ⊢ 𝐴 ∈ { 𝐴 , 𝐵 }
4 ffvelrn ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
5 3 4 mpan2 ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
6 5 adantr ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
7 2 prid2 ⊢ 𝐵 ∈ { 𝐴 , 𝐵 }
8 ffvelrn ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝑅 )
9 7 8 mpan2 ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 → ( 𝐹 ‘ 𝐵 ) ∈ 𝑅 )
10 9 adantr ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝑅 )
11 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
12 1 11 fvpr1 ⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
13 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
14 2 13 fvpr2 ⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
15 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
16 fveq2 ⊢ ( 𝑥 = 𝐴 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) ) )
18 eqcom ⊢ ( ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) ↔ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
19 17 18 bitrdi ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) )
20 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
21 fveq2 ⊢ ( 𝑥 = 𝐵 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) )
22 20 21 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) ) )
23 eqcom ⊢ ( ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) ↔ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
24 22 23 bitrdi ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) )
25 1 2 19 24 ralpr ⊢ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ↔ ( ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) )
26 12 14 25 sylanbrc ⊢ ( 𝐴 ≠ 𝐵 → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) )
27 26 adantl ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) )
28 ffn ⊢ ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 → 𝐹 Fn { 𝐴 , 𝐵 } )
29 1 2 11 13 fpr ⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } : { 𝐴 , 𝐵 } ⟶ { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) } )
30 29 ffnd ⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } )
31 eqfnfv ⊢ ( ( 𝐹 Fn { 𝐴 , 𝐵 } ∧ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } Fn { 𝐴 , 𝐵 } ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ) )
32 28 30 31 syl2an ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ‘ 𝑥 ) ) )
33 27 32 mpbird ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
34 opeq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
35 34 preq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } )
36 35 eqeq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ( 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ) )
37 opeq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ⟨ 𝐵 , 𝑦 ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
38 37 preq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
39 38 eqeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
40 36 39 rspc2ev ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝑅 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } )
41 6 10 33 40 syl3anc ⊢ ( ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } )
42 41 expcom ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ) )
43 vex ⊢ 𝑥 ∈ V
44 vex ⊢ 𝑦 ∈ V
45 1 2 43 44 fpr ⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝑥 , 𝑦 } )
46 prssi ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → { 𝑥 , 𝑦 } ⊆ 𝑅 )
47 fss ⊢ ( ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝑥 , 𝑦 } ∧ { 𝑥 , 𝑦 } ⊆ 𝑅 ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑅 )
48 45 46 47 syl2an ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑅 )
49 48 ex ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑅 ) )
50 feq1 ⊢ ( 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ↔ { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑅 ) )
51 50 biimprcd ⊢ ( { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑅 → ( 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ) )
52 49 51 syl6 ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ) ) )
53 52 rexlimdvv ⊢ ( 𝐴 ≠ 𝐵 → ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } → 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ) )
54 42 53 impbid ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐹 : { 𝐴 , 𝐵 } ⟶ 𝑅 ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑅 𝐹 = { ⟨ 𝐴 , 𝑥 ⟩ , ⟨ 𝐵 , 𝑦 ⟩ } ) )