Proof of Theorem ofoprabco
Step | Hyp | Ref
| Expression |
1 | | ofoprabco.5 |
. . . . . 6
⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
2 | | ofoprabco.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
3 | 2 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ 𝐵) |
4 | | ofoprabco.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
5 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐺‘𝑎) ∈ 𝐶) |
6 | | opelxpi 5072 |
. . . . . . 7
⊢ (((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐺‘𝑎) ∈ 𝐶) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (𝐵 × 𝐶)) |
7 | 3, 5, 6 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ (𝐵 × 𝐶)) |
8 | 1, 7 | fvmpt2d 6202 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑀‘𝑎) = 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
9 | 8 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
10 | | df-ov 6552 |
. . . . 5
⊢ ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = (𝑁‘〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) |
12 | | ofoprabco.6 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
14 | | simprl 790 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑥 = (𝐹‘𝑎)) |
15 | | simprr 792 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → 𝑦 = (𝐺‘𝑎)) |
16 | 14, 15 | oveq12d 6567 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ (𝑥 = (𝐹‘𝑎) ∧ 𝑦 = (𝐺‘𝑎))) → (𝑥𝑅𝑦) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
17 | | ovex 6577 |
. . . . . 6
⊢ ((𝐹‘𝑎)𝑅(𝐺‘𝑎)) ∈ V |
18 | 17 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑅(𝐺‘𝑎)) ∈ V) |
19 | 13, 16, 3, 5, 18 | ovmpt2d 6686 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐹‘𝑎)𝑁(𝐺‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
20 | 9, 11, 19 | 3eqtr2d 2650 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑁‘(𝑀‘𝑎)) = ((𝐹‘𝑎)𝑅(𝐺‘𝑎))) |
21 | 20 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎))) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))) |
22 | | ovex 6577 |
. . . . . 6
⊢ (𝑥𝑅𝑦) ∈ V |
23 | 22 | rgen2w 2909 |
. . . . 5
⊢
∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V |
24 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)) |
25 | 24 | fmpt2 7126 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦) ∈ V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V) |
26 | 23, 25 | mpbi 219 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V |
27 | 12 | feq1d 5943 |
. . . 4
⊢ (𝜑 → (𝑁:(𝐵 × 𝐶)⟶V ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)):(𝐵 × 𝐶)⟶V)) |
28 | 26, 27 | mpbiri 247 |
. . 3
⊢ (𝜑 → 𝑁:(𝐵 × 𝐶)⟶V) |
29 | 1, 7 | fmpt3d 6293 |
. . 3
⊢ (𝜑 → 𝑀:𝐴⟶(𝐵 × 𝐶)) |
30 | | ofoprabco.1 |
. . . 4
⊢
Ⅎ𝑎𝑀 |
31 | 30 | fcomptf 28840 |
. . 3
⊢ ((𝑁:(𝐵 × 𝐶)⟶V ∧ 𝑀:𝐴⟶(𝐵 × 𝐶)) → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎)))) |
32 | 28, 29, 31 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑁 ∘ 𝑀) = (𝑎 ∈ 𝐴 ↦ (𝑁‘(𝑀‘𝑎)))) |
33 | | ofoprabco.4 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
34 | 2 | feqmptd 6159 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝐹‘𝑎))) |
35 | 4 | feqmptd 6159 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑎 ∈ 𝐴 ↦ (𝐺‘𝑎))) |
36 | 33, 3, 5, 34, 35 | offval2 6812 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑎 ∈ 𝐴 ↦ ((𝐹‘𝑎)𝑅(𝐺‘𝑎)))) |
37 | 21, 32, 36 | 3eqtr4rd 2655 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑁 ∘ 𝑀)) |