Proof of Theorem ofoprabco
Step | Hyp | Ref
| Expression |
1 | | ofoprabco.5 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
2 | | ofoprabco.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
3 | 2 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝐵) |
4 | | ofoprabco.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
5 | 4 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ 𝐶) |
6 | | opelxpi 5588 |
. . . . . . 7
⊢ (((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐺‘𝑎) ∈ 𝐶) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (𝐵 × 𝐶)) |
7 | 3, 5, 6 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (𝐵 × 𝐶)) |
8 | 1, 7 | fvmpt2d 6831 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑀‘𝑎) = 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
9 | 8 | fveq2d 6721 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
10 | | df-ov 7216 |
. . . . 5
⊢ ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
12 | | ofoprabco.6 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
14 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑥 = (𝐹‘𝑎)) |
15 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑦 = (𝐺‘𝑎)) |
16 | 14, 15 | oveq12d 7231 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → (𝑥𝑅𝑦) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
17 | | ovexd 7248 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑅(𝐺‘𝑎)) ∈ V) |
18 | 13, 16, 3, 5, 17 | ovmpod 7361 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
19 | 9, 11, 18 | 3eqtr2d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
20 | 19 | mpteq2dva 5150 |
. 2
⊢ (𝜑 → (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))) |
21 | | ovex 7246 |
. . . . . 6
⊢ (𝑥𝑅𝑦) ∈ V |
22 | 21 | rgen2w 3074 |
. . . . 5
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V |
23 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)) |
24 | 23 | fmpo 7838 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V) |
25 | 22, 24 | mpbi 233 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V |
26 | 12 | feq1d 6530 |
. . . 4
⊢ (𝜑 → (𝑁:(𝐵 × 𝐶)⟶V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V)) |
27 | 25, 26 | mpbiri 261 |
. . 3
⊢ (𝜑 → 𝑁:(𝐵 × 𝐶)⟶V) |
28 | 1, 7 | fmpt3d 6933 |
. . 3
⊢ (𝜑 → 𝑀:𝐴⟶(𝐵 × 𝐶)) |
29 | | ofoprabco.1 |
. . . 4
⊢
Ⅎ𝑎𝑀 |
30 | 29 | fcomptf 30715 |
. . 3
⊢ ((𝑁:(𝐵 × 𝐶)⟶V ∧ 𝑀:𝐴⟶(𝐵 × 𝐶)) → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎)))) |
31 | 27, 28, 30 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎)))) |
32 | | ofoprabco.4 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
33 | 2 | feqmptd 6780 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
34 | 4 | feqmptd 6780 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑎 ∈ 𝐴 ↦ (𝐺‘𝑎))) |
35 | 32, 3, 5, 33, 34 | offval2 7488 |
. 2
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))) |
36 | 20, 31, 35 | 3eqtr4rd 2788 |
1
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀)) |