Step | Hyp | Ref
| Expression |
1 | | caoftrn.5 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) |
2 | 1 | ralrimivvva 2553 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) |
3 | 2 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) |
4 | | caofref.2 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
5 | 4 | ffvelrnda 5631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) ∈ 𝑆) |
6 | | caofcom.3 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐴⟶𝑆) |
7 | 6 | ffvelrnda 5631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑆) |
8 | | caofass.4 |
. . . . . 6
⊢ (𝜑 → 𝐻:𝐴⟶𝑆) |
9 | 8 | ffvelrnda 5631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) ∈ 𝑆) |
10 | | breq1 3992 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑤) → (𝑥𝑅𝑦 ↔ (𝐹‘𝑤)𝑅𝑦)) |
11 | 10 | anbi1d 462 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑤) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) ↔ ((𝐹‘𝑤)𝑅𝑦 ∧ 𝑦𝑇𝑧))) |
12 | | breq1 3992 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑤) → (𝑥𝑈𝑧 ↔ (𝐹‘𝑤)𝑈𝑧)) |
13 | 11, 12 | imbi12d 233 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑤) → (((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧) ↔ (((𝐹‘𝑤)𝑅𝑦 ∧ 𝑦𝑇𝑧) → (𝐹‘𝑤)𝑈𝑧))) |
14 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑤) → ((𝐹‘𝑤)𝑅𝑦 ↔ (𝐹‘𝑤)𝑅(𝐺‘𝑤))) |
15 | | breq1 3992 |
. . . . . . . 8
⊢ (𝑦 = (𝐺‘𝑤) → (𝑦𝑇𝑧 ↔ (𝐺‘𝑤)𝑇𝑧)) |
16 | 14, 15 | anbi12d 470 |
. . . . . . 7
⊢ (𝑦 = (𝐺‘𝑤) → (((𝐹‘𝑤)𝑅𝑦 ∧ 𝑦𝑇𝑧) ↔ ((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇𝑧))) |
17 | 16 | imbi1d 230 |
. . . . . 6
⊢ (𝑦 = (𝐺‘𝑤) → ((((𝐹‘𝑤)𝑅𝑦 ∧ 𝑦𝑇𝑧) → (𝐹‘𝑤)𝑈𝑧) ↔ (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇𝑧) → (𝐹‘𝑤)𝑈𝑧))) |
18 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑧 = (𝐻‘𝑤) → ((𝐺‘𝑤)𝑇𝑧 ↔ (𝐺‘𝑤)𝑇(𝐻‘𝑤))) |
19 | 18 | anbi2d 461 |
. . . . . . 7
⊢ (𝑧 = (𝐻‘𝑤) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇𝑧) ↔ ((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)))) |
20 | | breq2 3993 |
. . . . . . 7
⊢ (𝑧 = (𝐻‘𝑤) → ((𝐹‘𝑤)𝑈𝑧 ↔ (𝐹‘𝑤)𝑈(𝐻‘𝑤))) |
21 | 19, 20 | imbi12d 233 |
. . . . . 6
⊢ (𝑧 = (𝐻‘𝑤) → ((((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇𝑧) → (𝐹‘𝑤)𝑈𝑧) ↔ (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) → (𝐹‘𝑤)𝑈(𝐻‘𝑤)))) |
22 | 13, 17, 21 | rspc3v 2850 |
. . . . 5
⊢ (((𝐹‘𝑤) ∈ 𝑆 ∧ (𝐺‘𝑤) ∈ 𝑆 ∧ (𝐻‘𝑤) ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) → (𝐹‘𝑤)𝑈(𝐻‘𝑤)))) |
23 | 5, 7, 9, 22 | syl3anc 1233 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) → (𝐹‘𝑤)𝑈(𝐻‘𝑤)))) |
24 | 3, 23 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) → (𝐹‘𝑤)𝑈(𝐻‘𝑤))) |
25 | 24 | ralimdva 2537 |
. 2
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) → ∀𝑤 ∈ 𝐴 (𝐹‘𝑤)𝑈(𝐻‘𝑤))) |
26 | | ffn 5347 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝑆 → 𝐹 Fn 𝐴) |
27 | 4, 26 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
28 | | ffn 5347 |
. . . . . 6
⊢ (𝐺:𝐴⟶𝑆 → 𝐺 Fn 𝐴) |
29 | 6, 28 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐺 Fn 𝐴) |
30 | | caofref.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
31 | | inidm 3336 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
32 | | eqidd 2171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) = (𝐹‘𝑤)) |
33 | | eqidd 2171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) = (𝐺‘𝑤)) |
34 | 27, 29, 30, 30, 31, 32, 33 | ofrfval 6069 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑤 ∈ 𝐴 (𝐹‘𝑤)𝑅(𝐺‘𝑤))) |
35 | | ffn 5347 |
. . . . . 6
⊢ (𝐻:𝐴⟶𝑆 → 𝐻 Fn 𝐴) |
36 | 8, 35 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn 𝐴) |
37 | | eqidd 2171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐻‘𝑤) = (𝐻‘𝑤)) |
38 | 29, 36, 30, 30, 31, 33, 37 | ofrfval 6069 |
. . . 4
⊢ (𝜑 → (𝐺 ∘𝑟 𝑇𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤)𝑇(𝐻‘𝑤))) |
39 | 34, 38 | anbi12d 470 |
. . 3
⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) ↔ (∀𝑤 ∈ 𝐴 (𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤)𝑇(𝐻‘𝑤)))) |
40 | | r19.26 2596 |
. . 3
⊢
(∀𝑤 ∈
𝐴 ((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)) ↔ (∀𝑤 ∈ 𝐴 (𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ ∀𝑤 ∈ 𝐴 (𝐺‘𝑤)𝑇(𝐻‘𝑤))) |
41 | 39, 40 | bitr4di 197 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) ↔ ∀𝑤 ∈ 𝐴 ((𝐹‘𝑤)𝑅(𝐺‘𝑤) ∧ (𝐺‘𝑤)𝑇(𝐻‘𝑤)))) |
42 | 27, 36, 30, 30, 31, 32, 37 | ofrfval 6069 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑟 𝑈𝐻 ↔ ∀𝑤 ∈ 𝐴 (𝐹‘𝑤)𝑈(𝐻‘𝑤))) |
43 | 25, 41, 42 | 3imtr4d 202 |
1
⊢ (𝜑 → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟 𝑇𝐻) → 𝐹 ∘𝑟 𝑈𝐻)) |