Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prfval Structured version   Visualization version   GIF version

Theorem prfval 17449
 Description: Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
prfval.k 𝑃 = (𝐹 ⟨,⟩F 𝐺)
prfval.b 𝐵 = (Base‘𝐶)
prfval.h 𝐻 = (Hom ‘𝐶)
prfval.c (𝜑𝐹 ∈ (𝐶 Func 𝐷))
prfval.d (𝜑𝐺 ∈ (𝐶 Func 𝐸))
Assertion
Ref Expression
prfval (𝜑𝑃 = ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
Distinct variable groups:   𝑥,,𝑦,𝐵   𝑥,𝐶,𝑦   ,𝐹,𝑥,𝑦   𝜑,,𝑥,𝑦   𝑥,𝐷,𝑦   ,𝐺,𝑥,𝑦   ,𝐻,𝑥,𝑦
Allowed substitution hints:   𝐶()   𝐷()   𝑃(𝑥,𝑦,)   𝐸(𝑥,𝑦,)

Proof of Theorem prfval
Dummy variables 𝑓 𝑏 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prfval.k . 2 𝑃 = (𝐹 ⟨,⟩F 𝐺)
2 df-prf 17425 . . . 4 ⟨,⟩F = (𝑓 ∈ V, 𝑔 ∈ V ↦ dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩)
32a1i 11 . . 3 (𝜑 → ⟨,⟩F = (𝑓 ∈ V, 𝑔 ∈ V ↦ dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩))
4 fvex 6674 . . . . . 6 (1st𝑓) ∈ V
54dmex 7611 . . . . 5 dom (1st𝑓) ∈ V
65a1i 11 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → dom (1st𝑓) ∈ V)
7 simprl 770 . . . . . . 7 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → 𝑓 = 𝐹)
87fveq2d 6665 . . . . . 6 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → (1st𝑓) = (1st𝐹))
98dmeqd 5761 . . . . 5 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → dom (1st𝑓) = dom (1st𝐹))
10 prfval.b . . . . . . . 8 𝐵 = (Base‘𝐶)
11 eqid 2824 . . . . . . . 8 (Base‘𝐷) = (Base‘𝐷)
12 relfunc 17132 . . . . . . . . 9 Rel (𝐶 Func 𝐷)
13 prfval.c . . . . . . . . 9 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
14 1st2ndbr 7736 . . . . . . . . 9 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
1512, 13, 14sylancr 590 . . . . . . . 8 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
1610, 11, 15funcf1 17136 . . . . . . 7 (𝜑 → (1st𝐹):𝐵⟶(Base‘𝐷))
1716fdmd 6513 . . . . . 6 (𝜑 → dom (1st𝐹) = 𝐵)
1817adantr 484 . . . . 5 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → dom (1st𝐹) = 𝐵)
199, 18eqtrd 2859 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → dom (1st𝑓) = 𝐵)
20 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
21 simplrl 776 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → 𝑓 = 𝐹)
2221fveq2d 6665 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (1st𝑓) = (1st𝐹))
2322fveq1d 6663 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → ((1st𝑓)‘𝑥) = ((1st𝐹)‘𝑥))
24 simplrr 777 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → 𝑔 = 𝐺)
2524fveq2d 6665 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (1st𝑔) = (1st𝐺))
2625fveq1d 6663 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → ((1st𝑔)‘𝑥) = ((1st𝐺)‘𝑥))
2723, 26opeq12d 4797 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)
2820, 27mpteq12dv 5137 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩) = (𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
29 eqidd 2825 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩) = ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))
3020, 20, 29mpoeq123dv 7222 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩)) = (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩)))
3121ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑓 = 𝐹)
3231fveq2d 6665 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd𝐹))
3332oveqd 7166 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑥(2nd𝐹)𝑦))
3433dmeqd 5761 . . . . . . . . . 10 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → dom (𝑥(2nd𝑓)𝑦) = dom (𝑥(2nd𝐹)𝑦))
35 prfval.h . . . . . . . . . . . 12 𝐻 = (Hom ‘𝐶)
36 eqid 2824 . . . . . . . . . . . 12 (Hom ‘𝐷) = (Hom ‘𝐷)
3715ad4antr 731 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
38 simplr 768 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑥𝐵)
39 simpr 488 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑦𝐵)
4010, 35, 36, 37, 38, 39funcf2 17138 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (𝑥(2nd𝐹)𝑦):(𝑥𝐻𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
4140fdmd 6513 . . . . . . . . . 10 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → dom (𝑥(2nd𝐹)𝑦) = (𝑥𝐻𝑦))
4234, 41eqtrd 2859 . . . . . . . . 9 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → dom (𝑥(2nd𝑓)𝑦) = (𝑥𝐻𝑦))
4333fveq1d 6663 . . . . . . . . . 10 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘) = ((𝑥(2nd𝐹)𝑦)‘))
4424ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → 𝑔 = 𝐺)
4544fveq2d 6665 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (2nd𝑔) = (2nd𝐺))
4645oveqd 7166 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → (𝑥(2nd𝑔)𝑦) = (𝑥(2nd𝐺)𝑦))
4746fveq1d 6663 . . . . . . . . . 10 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ((𝑥(2nd𝑔)𝑦)‘) = ((𝑥(2nd𝐺)𝑦)‘))
4843, 47opeq12d 4797 . . . . . . . . 9 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩ = ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)
4942, 48mpteq12dv 5137 . . . . . . . 8 (((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵) ∧ 𝑦𝐵) → ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩) = ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
50493impa 1107 . . . . . . 7 ((((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) ∧ 𝑥𝐵𝑦𝐵) → ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩) = ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
5150mpoeq3dva 7224 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩)) = (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)))
5230, 51eqtrd 2859 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩)) = (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)))
5328, 52opeq12d 4797 . . . 4 (((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) ∧ 𝑏 = 𝐵) → ⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩ = ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
546, 19, 53csbied2 3903 . . 3 ((𝜑 ∧ (𝑓 = 𝐹𝑔 = 𝐺)) → dom (1st𝑓) / 𝑏⟨(𝑥𝑏 ↦ ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩), (𝑥𝑏, 𝑦𝑏 ↦ ( ∈ dom (𝑥(2nd𝑓)𝑦) ↦ ⟨((𝑥(2nd𝑓)𝑦)‘), ((𝑥(2nd𝑔)𝑦)‘)⟩))⟩ = ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
5513elexd 3500 . . 3 (𝜑𝐹 ∈ V)
56 prfval.d . . . 4 (𝜑𝐺 ∈ (𝐶 Func 𝐸))
5756elexd 3500 . . 3 (𝜑𝐺 ∈ V)
58 opex 5343 . . . 4 ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩ ∈ V
5958a1i 11 . . 3 (𝜑 → ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩ ∈ V)
603, 54, 55, 57, 59ovmpod 7295 . 2 (𝜑 → (𝐹 ⟨,⟩F 𝐺) = ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
611, 60syl5eq 2871 1 (𝜑𝑃 = ⟨(𝑥𝐵 ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥𝐵, 𝑦𝐵 ↦ ( ∈ (𝑥𝐻𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  Vcvv 3480  ⦋csb 3866  ⟨cop 4556   class class class wbr 5052   ↦ cmpt 5132  dom cdm 5542  Rel wrel 5547  ‘cfv 6343  (class class class)co 7149   ∈ cmpo 7151  1st c1st 7682  2nd c2nd 7683  Basecbs 16483  Hom chom 16576   Func cfunc 17124   ⟨,⟩F cprf 17421 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7684  df-2nd 7685  df-map 8404  df-ixp 8458  df-func 17128  df-prf 17425 This theorem is referenced by:  prf1  17450  prf2fval  17451  prfcl  17453  prf1st  17454  prf2nd  17455  1st2ndprf  17456
 Copyright terms: Public domain W3C validator