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

Theorem off 7402
 Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
off.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
off.2 (𝜑𝐹:𝐴𝑆)
off.3 (𝜑𝐺:𝐵𝑇)
off.4 (𝜑𝐴𝑉)
off.5 (𝜑𝐵𝑊)
off.6 (𝐴𝐵) = 𝐶
Assertion
Ref Expression
off (𝜑 → (𝐹f 𝑅𝐺):𝐶𝑈)
Distinct variable groups:   𝑦,𝐺   𝑥,𝑦,𝜑   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐺(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem off
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . 4 (𝜑𝐹:𝐴𝑆)
21ffnd 6491 . . 3 (𝜑𝐹 Fn 𝐴)
3 off.3 . . . 4 (𝜑𝐺:𝐵𝑇)
43ffnd 6491 . . 3 (𝜑𝐺 Fn 𝐵)
5 off.4 . . 3 (𝜑𝐴𝑉)
6 off.5 . . 3 (𝜑𝐵𝑊)
7 off.6 . . 3 (𝐴𝐵) = 𝐶
8 eqidd 2821 . . 3 ((𝜑𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
9 eqidd 2821 . . 3 ((𝜑𝑧𝐵) → (𝐺𝑧) = (𝐺𝑧))
102, 4, 5, 6, 7, 8, 9offval 7394 . 2 (𝜑 → (𝐹f 𝑅𝐺) = (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))))
11 inss1 4183 . . . . . 6 (𝐴𝐵) ⊆ 𝐴
127, 11eqsstrri 3981 . . . . 5 𝐶𝐴
1312sseli 3942 . . . 4 (𝑧𝐶𝑧𝐴)
14 ffvelrn 6825 . . . 4 ((𝐹:𝐴𝑆𝑧𝐴) → (𝐹𝑧) ∈ 𝑆)
151, 13, 14syl2an 597 . . 3 ((𝜑𝑧𝐶) → (𝐹𝑧) ∈ 𝑆)
16 inss2 4184 . . . . . 6 (𝐴𝐵) ⊆ 𝐵
177, 16eqsstrri 3981 . . . . 5 𝐶𝐵
1817sseli 3942 . . . 4 (𝑧𝐶𝑧𝐵)
19 ffvelrn 6825 . . . 4 ((𝐺:𝐵𝑇𝑧𝐵) → (𝐺𝑧) ∈ 𝑇)
203, 18, 19syl2an 597 . . 3 ((𝜑𝑧𝐶) → (𝐺𝑧) ∈ 𝑇)
21 off.1 . . . . 5 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
2221ralrimivva 3178 . . . 4 (𝜑 → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
2322adantr 483 . . 3 ((𝜑𝑧𝐶) → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
24 ovrspc2v 7159 . . 3 ((((𝐹𝑧) ∈ 𝑆 ∧ (𝐺𝑧) ∈ 𝑇) ∧ ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2515, 20, 23, 24syl21anc 835 . 2 ((𝜑𝑧𝐶) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2610, 25fmpt3d 6856 1 (𝜑 → (𝐹f 𝑅𝐺):𝐶𝑈)