Step | Hyp | Ref
| Expression |
1 | | ofun.a |
. . . 4
⊢ (𝜑 → 𝐴 Fn 𝑀) |
2 | | ofun.c |
. . . 4
⊢ (𝜑 → 𝐶 Fn 𝑁) |
3 | | ofun.1 |
. . . 4
⊢ (𝜑 → (𝑀 ∩ 𝑁) = ∅) |
4 | 1, 2, 3 | fnund 6439 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐶) Fn (𝑀 ∪ 𝑁)) |
5 | | ofun.b |
. . . 4
⊢ (𝜑 → 𝐵 Fn 𝑀) |
6 | | ofun.d |
. . . 4
⊢ (𝜑 → 𝐷 Fn 𝑁) |
7 | 5, 6, 3 | fnund 6439 |
. . 3
⊢ (𝜑 → (𝐵 ∪ 𝐷) Fn (𝑀 ∪ 𝑁)) |
8 | | ofun.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑉) |
9 | | ofun.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑊) |
10 | 8, 9 | unexd 7468 |
. . 3
⊢ (𝜑 → (𝑀 ∪ 𝑁) ∈ V) |
11 | | inidm 4119 |
. . 3
⊢ ((𝑀 ∪ 𝑁) ∩ (𝑀 ∪ 𝑁)) = (𝑀 ∪ 𝑁) |
12 | 4, 7, 10, 10, 11 | offn 7410 |
. 2
⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) Fn (𝑀 ∪ 𝑁)) |
13 | | inidm 4119 |
. . . 4
⊢ (𝑀 ∩ 𝑀) = 𝑀 |
14 | 1, 5, 8, 8, 13 | offn 7410 |
. . 3
⊢ (𝜑 → (𝐴 ∘f 𝑅𝐵) Fn 𝑀) |
15 | | inidm 4119 |
. . . 4
⊢ (𝑁 ∩ 𝑁) = 𝑁 |
16 | 2, 6, 9, 9, 15 | offn 7410 |
. . 3
⊢ (𝜑 → (𝐶 ∘f 𝑅𝐷) Fn 𝑁) |
17 | 14, 16, 3 | fnund 6439 |
. 2
⊢ (𝜑 → ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷)) Fn (𝑀 ∪ 𝑁)) |
18 | | eqidd 2760 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀 ∪ 𝑁)) → ((𝐴 ∪ 𝐶)‘𝑥) = ((𝐴 ∪ 𝐶)‘𝑥)) |
19 | | eqidd 2760 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀 ∪ 𝑁)) → ((𝐵 ∪ 𝐷)‘𝑥) = ((𝐵 ∪ 𝐷)‘𝑥)) |
20 | 4, 7, 10, 10, 11, 18, 19 | ofval 7408 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀 ∪ 𝑁)) → (((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷))‘𝑥) = (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥))) |
21 | | elun 4050 |
. . . 4
⊢ (𝑥 ∈ (𝑀 ∪ 𝑁) ↔ (𝑥 ∈ 𝑀 ∨ 𝑥 ∈ 𝑁)) |
22 | | eqidd 2760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (𝐴‘𝑥) = (𝐴‘𝑥)) |
23 | | eqidd 2760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (𝐵‘𝑥) = (𝐵‘𝑥)) |
24 | 1, 5, 8, 8, 13, 22, 23 | ofval 7408 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ((𝐴 ∘f 𝑅𝐵)‘𝑥) = ((𝐴‘𝑥)𝑅(𝐵‘𝑥))) |
25 | 14 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (𝐴 ∘f 𝑅𝐵) Fn 𝑀) |
26 | 16 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (𝐶 ∘f 𝑅𝐷) Fn 𝑁) |
27 | 3 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (𝑀 ∩ 𝑁) = ∅) |
28 | | simpr 489 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → 𝑥 ∈ 𝑀) |
29 | 25, 26, 27, 28 | fvun1d 6738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥) = ((𝐴 ∘f 𝑅𝐵)‘𝑥)) |
30 | 1 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → 𝐴 Fn 𝑀) |
31 | 2 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → 𝐶 Fn 𝑁) |
32 | 30, 31, 27, 28 | fvun1d 6738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ((𝐴 ∪ 𝐶)‘𝑥) = (𝐴‘𝑥)) |
33 | 5 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → 𝐵 Fn 𝑀) |
34 | 6 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → 𝐷 Fn 𝑁) |
35 | 33, 34, 27, 28 | fvun1d 6738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ((𝐵 ∪ 𝐷)‘𝑥) = (𝐵‘𝑥)) |
36 | 32, 35 | oveq12d 7161 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = ((𝐴‘𝑥)𝑅(𝐵‘𝑥))) |
37 | 24, 29, 36 | 3eqtr4rd 2805 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥)) |
38 | | eqidd 2760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (𝐶‘𝑥) = (𝐶‘𝑥)) |
39 | | eqidd 2760 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (𝐷‘𝑥) = (𝐷‘𝑥)) |
40 | 2, 6, 9, 9, 15, 38, 39 | ofval 7408 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → ((𝐶 ∘f 𝑅𝐷)‘𝑥) = ((𝐶‘𝑥)𝑅(𝐷‘𝑥))) |
41 | 14 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (𝐴 ∘f 𝑅𝐵) Fn 𝑀) |
42 | 16 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (𝐶 ∘f 𝑅𝐷) Fn 𝑁) |
43 | 3 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (𝑀 ∩ 𝑁) = ∅) |
44 | | simpr 489 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝑥 ∈ 𝑁) |
45 | 41, 42, 43, 44 | fvun2d 6739 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥) = ((𝐶 ∘f 𝑅𝐷)‘𝑥)) |
46 | 1 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝐴 Fn 𝑀) |
47 | 2 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝐶 Fn 𝑁) |
48 | 46, 47, 43, 44 | fvun2d 6739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → ((𝐴 ∪ 𝐶)‘𝑥) = (𝐶‘𝑥)) |
49 | 5 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝐵 Fn 𝑀) |
50 | 6 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → 𝐷 Fn 𝑁) |
51 | 49, 50, 43, 44 | fvun2d 6739 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → ((𝐵 ∪ 𝐷)‘𝑥) = (𝐷‘𝑥)) |
52 | 48, 51 | oveq12d 7161 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = ((𝐶‘𝑥)𝑅(𝐷‘𝑥))) |
53 | 40, 45, 52 | 3eqtr4rd 2805 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥)) |
54 | 37, 53 | jaodan 956 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑀 ∨ 𝑥 ∈ 𝑁)) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥)) |
55 | 21, 54 | sylan2b 597 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀 ∪ 𝑁)) → (((𝐴 ∪ 𝐶)‘𝑥)𝑅((𝐵 ∪ 𝐷)‘𝑥)) = (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥)) |
56 | 20, 55 | eqtrd 2794 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀 ∪ 𝑁)) → (((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷))‘𝑥) = (((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))‘𝑥)) |
57 | 12, 17, 56 | eqfnfvd 6789 |
1
⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) = ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))) |