Step | Hyp | Ref
| Expression |
1 | | caoftrn.5 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝑅y ∧ y𝑇z) → x𝑈z)) |
2 | 1 | ralrimivvva 2396 |
. . . . 5
⊢ (φ → ∀x ∈ 𝑆 ∀y ∈ 𝑆 ∀z ∈ 𝑆 ((x𝑅y ∧ y𝑇z) → x𝑈z)) |
3 | 2 | adantr 261 |
. . . 4
⊢ ((φ ∧ w ∈ A) → ∀x ∈ 𝑆 ∀y ∈ 𝑆 ∀z ∈ 𝑆 ((x𝑅y ∧ y𝑇z) → x𝑈z)) |
4 | | caofref.2 |
. . . . . 6
⊢ (φ → 𝐹:A⟶𝑆) |
5 | 4 | ffvelrnda 5245 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐹‘w) ∈ 𝑆) |
6 | | caofcom.3 |
. . . . . 6
⊢ (φ → 𝐺:A⟶𝑆) |
7 | 6 | ffvelrnda 5245 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐺‘w) ∈ 𝑆) |
8 | | caofass.4 |
. . . . . 6
⊢ (φ → 𝐻:A⟶𝑆) |
9 | 8 | ffvelrnda 5245 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐻‘w) ∈ 𝑆) |
10 | | breq1 3758 |
. . . . . . . 8
⊢ (x = (𝐹‘w) → (x𝑅y ↔
(𝐹‘w)𝑅y)) |
11 | 10 | anbi1d 438 |
. . . . . . 7
⊢ (x = (𝐹‘w) → ((x𝑅y ∧ y𝑇z) ↔ ((𝐹‘w)𝑅y ∧ y𝑇z))) |
12 | | breq1 3758 |
. . . . . . 7
⊢ (x = (𝐹‘w) → (x𝑈z ↔
(𝐹‘w)𝑈z)) |
13 | 11, 12 | imbi12d 223 |
. . . . . 6
⊢ (x = (𝐹‘w) → (((x𝑅y ∧ y𝑇z) → x𝑈z) ↔ (((𝐹‘w)𝑅y ∧ y𝑇z) → (𝐹‘w)𝑈z))) |
14 | | breq2 3759 |
. . . . . . . 8
⊢ (y = (𝐺‘w) → ((𝐹‘w)𝑅y ↔
(𝐹‘w)𝑅(𝐺‘w))) |
15 | | breq1 3758 |
. . . . . . . 8
⊢ (y = (𝐺‘w) → (y𝑇z ↔
(𝐺‘w)𝑇z)) |
16 | 14, 15 | anbi12d 442 |
. . . . . . 7
⊢ (y = (𝐺‘w) → (((𝐹‘w)𝑅y ∧ y𝑇z) ↔ ((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇z))) |
17 | 16 | imbi1d 220 |
. . . . . 6
⊢ (y = (𝐺‘w) → ((((𝐹‘w)𝑅y ∧ y𝑇z) → (𝐹‘w)𝑈z)
↔ (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇z)
→ (𝐹‘w)𝑈z))) |
18 | | breq2 3759 |
. . . . . . . 8
⊢ (z = (𝐻‘w) → ((𝐺‘w)𝑇z ↔
(𝐺‘w)𝑇(𝐻‘w))) |
19 | 18 | anbi2d 437 |
. . . . . . 7
⊢ (z = (𝐻‘w) → (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇z)
↔ ((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)))) |
20 | | breq2 3759 |
. . . . . . 7
⊢ (z = (𝐻‘w) → ((𝐹‘w)𝑈z ↔
(𝐹‘w)𝑈(𝐻‘w))) |
21 | 19, 20 | imbi12d 223 |
. . . . . 6
⊢ (z = (𝐻‘w) → ((((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇z)
→ (𝐹‘w)𝑈z)
↔ (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) → (𝐹‘w)𝑈(𝐻‘w)))) |
22 | 13, 17, 21 | rspc3v 2659 |
. . . . 5
⊢ (((𝐹‘w) ∈ 𝑆 ∧ (𝐺‘w) ∈ 𝑆 ∧ (𝐻‘w) ∈ 𝑆) → (∀x ∈ 𝑆 ∀y ∈ 𝑆 ∀z ∈ 𝑆 ((x𝑅y ∧ y𝑇z) → x𝑈z) → (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) → (𝐹‘w)𝑈(𝐻‘w)))) |
23 | 5, 7, 9, 22 | syl3anc 1134 |
. . . 4
⊢ ((φ ∧ w ∈ A) → (∀x ∈ 𝑆 ∀y ∈ 𝑆 ∀z ∈ 𝑆 ((x𝑅y ∧ y𝑇z) → x𝑈z) → (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) → (𝐹‘w)𝑈(𝐻‘w)))) |
24 | 3, 23 | mpd 13 |
. . 3
⊢ ((φ ∧ w ∈ A) → (((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) → (𝐹‘w)𝑈(𝐻‘w))) |
25 | 24 | ralimdva 2381 |
. 2
⊢ (φ → (∀w ∈ A ((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) → ∀w ∈ A (𝐹‘w)𝑈(𝐻‘w))) |
26 | | ffn 4989 |
. . . . . 6
⊢ (𝐹:A⟶𝑆 → 𝐹 Fn A) |
27 | 4, 26 | syl 14 |
. . . . 5
⊢ (φ → 𝐹 Fn A) |
28 | | ffn 4989 |
. . . . . 6
⊢ (𝐺:A⟶𝑆 → 𝐺 Fn A) |
29 | 6, 28 | syl 14 |
. . . . 5
⊢ (φ → 𝐺 Fn A) |
30 | | caofref.1 |
. . . . 5
⊢ (φ → A ∈ 𝑉) |
31 | | inidm 3140 |
. . . . 5
⊢ (A ∩ A) =
A |
32 | | eqidd 2038 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐹‘w) = (𝐹‘w)) |
33 | | eqidd 2038 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐺‘w) = (𝐺‘w)) |
34 | 27, 29, 30, 30, 31, 32, 33 | ofrfval 5662 |
. . . 4
⊢ (φ → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀w ∈ A (𝐹‘w)𝑅(𝐺‘w))) |
35 | | ffn 4989 |
. . . . . 6
⊢ (𝐻:A⟶𝑆 → 𝐻 Fn A) |
36 | 8, 35 | syl 14 |
. . . . 5
⊢ (φ → 𝐻 Fn A) |
37 | | eqidd 2038 |
. . . . 5
⊢ ((φ ∧ w ∈ A) → (𝐻‘w) = (𝐻‘w)) |
38 | 29, 36, 30, 30, 31, 33, 37 | ofrfval 5662 |
. . . 4
⊢ (φ → (𝐺 ∘𝑟 𝑇𝐻 ↔ ∀w ∈ A (𝐺‘w)𝑇(𝐻‘w))) |
39 | 34, 38 | anbi12d 442 |
. . 3
⊢ (φ → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟
𝑇𝐻) ↔ (∀w ∈ A (𝐹‘w)𝑅(𝐺‘w) ∧ ∀w ∈ A (𝐺‘w)𝑇(𝐻‘w)))) |
40 | | r19.26 2435 |
. . 3
⊢ (∀w ∈ A ((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)) ↔ (∀w ∈ A (𝐹‘w)𝑅(𝐺‘w) ∧ ∀w ∈ A (𝐺‘w)𝑇(𝐻‘w))) |
41 | 39, 40 | syl6bbr 187 |
. 2
⊢ (φ → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟
𝑇𝐻) ↔ ∀w ∈ A ((𝐹‘w)𝑅(𝐺‘w) ∧ (𝐺‘w)𝑇(𝐻‘w)))) |
42 | 27, 36, 30, 30, 31, 32, 37 | ofrfval 5662 |
. 2
⊢ (φ → (𝐹 ∘𝑟 𝑈𝐻 ↔ ∀w ∈ A (𝐹‘w)𝑈(𝐻‘w))) |
43 | 25, 41, 42 | 3imtr4d 192 |
1
⊢ (φ → ((𝐹 ∘𝑟 𝑅𝐺 ∧ 𝐺 ∘𝑟
𝑇𝐻) → 𝐹 ∘𝑟 𝑈𝐻)) |