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

Theorem off 7063
 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 (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)
Distinct variable groups:   𝑦,𝐺   𝑥,𝑦,𝜑   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐺(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem off
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 off.2 . . . . 5 (𝜑𝐹:𝐴𝑆)
2 off.6 . . . . . . 7 (𝐴𝐵) = 𝐶
3 inss1 3981 . . . . . . 7 (𝐴𝐵) ⊆ 𝐴
42, 3eqsstr3i 3785 . . . . . 6 𝐶𝐴
54sseli 3748 . . . . 5 (𝑧𝐶𝑧𝐴)
6 ffvelrn 6502 . . . . 5 ((𝐹:𝐴𝑆𝑧𝐴) → (𝐹𝑧) ∈ 𝑆)
71, 5, 6syl2an 583 . . . 4 ((𝜑𝑧𝐶) → (𝐹𝑧) ∈ 𝑆)
8 off.3 . . . . 5 (𝜑𝐺:𝐵𝑇)
9 inss2 3982 . . . . . . 7 (𝐴𝐵) ⊆ 𝐵
102, 9eqsstr3i 3785 . . . . . 6 𝐶𝐵
1110sseli 3748 . . . . 5 (𝑧𝐶𝑧𝐵)
12 ffvelrn 6502 . . . . 5 ((𝐺:𝐵𝑇𝑧𝐵) → (𝐺𝑧) ∈ 𝑇)
138, 11, 12syl2an 583 . . . 4 ((𝜑𝑧𝐶) → (𝐺𝑧) ∈ 𝑇)
14 off.1 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
1514ralrimivva 3120 . . . . 5 (𝜑 → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
1615adantr 466 . . . 4 ((𝜑𝑧𝐶) → ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈)
17 oveq1 6803 . . . . . 6 (𝑥 = (𝐹𝑧) → (𝑥𝑅𝑦) = ((𝐹𝑧)𝑅𝑦))
1817eleq1d 2835 . . . . 5 (𝑥 = (𝐹𝑧) → ((𝑥𝑅𝑦) ∈ 𝑈 ↔ ((𝐹𝑧)𝑅𝑦) ∈ 𝑈))
19 oveq2 6804 . . . . . 6 (𝑦 = (𝐺𝑧) → ((𝐹𝑧)𝑅𝑦) = ((𝐹𝑧)𝑅(𝐺𝑧)))
2019eleq1d 2835 . . . . 5 (𝑦 = (𝐺𝑧) → (((𝐹𝑧)𝑅𝑦) ∈ 𝑈 ↔ ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈))
2118, 20rspc2va 3473 . . . 4 ((((𝐹𝑧) ∈ 𝑆 ∧ (𝐺𝑧) ∈ 𝑇) ∧ ∀𝑥𝑆𝑦𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
227, 13, 16, 21syl21anc 1475 . . 3 ((𝜑𝑧𝐶) → ((𝐹𝑧)𝑅(𝐺𝑧)) ∈ 𝑈)
2322fmpttd 6530 . 2 (𝜑 → (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))):𝐶𝑈)
241ffnd 6185 . . . 4 (𝜑𝐹 Fn 𝐴)
258ffnd 6185 . . . 4 (𝜑𝐺 Fn 𝐵)
26 off.4 . . . 4 (𝜑𝐴𝑉)
27 off.5 . . . 4 (𝜑𝐵𝑊)
28 eqidd 2772 . . . 4 ((𝜑𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
29 eqidd 2772 . . . 4 ((𝜑𝑧𝐵) → (𝐺𝑧) = (𝐺𝑧))
3024, 25, 26, 27, 2, 28, 29offval 7055 . . 3 (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))))
3130feq1d 6169 . 2 (𝜑 → ((𝐹𝑓 𝑅𝐺):𝐶𝑈 ↔ (𝑧𝐶 ↦ ((𝐹𝑧)𝑅(𝐺𝑧))):𝐶𝑈))
3223, 31mpbird 247 1 (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)