Step | Hyp | Ref
| Expression |
1 | | caofref.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | caofinv.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁:𝑆⟶𝑆) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑁:𝑆⟶𝑆) |
4 | | caofref.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
5 | 4 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ 𝑆) |
6 | 3, 5 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝑁‘(𝐹‘𝑣)) ∈ 𝑆) |
7 | | eqid 2622 |
. . . . . . 7
⊢ (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))) = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))) |
8 | 6, 7 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))):𝐴⟶𝑆) |
9 | | caofinv.5 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) |
10 | 9 | feq1d 6030 |
. . . . . 6
⊢ (𝜑 → (𝐺:𝐴⟶𝑆 ↔ (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))):𝐴⟶𝑆)) |
11 | 8, 10 | mpbird 247 |
. . . . 5
⊢ (𝜑 → 𝐺:𝐴⟶𝑆) |
12 | 11 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) ∈ 𝑆) |
13 | 4 | ffvelrnda 6359 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘𝑤) ∈ 𝑆) |
14 | | fvex 6201 |
. . . . . . 7
⊢ (𝑁‘(𝐹‘𝑣)) ∈ V |
15 | 14, 7 | fnmpti 6022 |
. . . . . 6
⊢ (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))) Fn 𝐴 |
16 | 9 | fneq1d 5981 |
. . . . . 6
⊢ (𝜑 → (𝐺 Fn 𝐴 ↔ (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣))) Fn 𝐴)) |
17 | 15, 16 | mpbiri 248 |
. . . . 5
⊢ (𝜑 → 𝐺 Fn 𝐴) |
18 | | dffn5 6241 |
. . . . 5
⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑤 ∈ 𝐴 ↦ (𝐺‘𝑤))) |
19 | 17, 18 | sylib 208 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑤 ∈ 𝐴 ↦ (𝐺‘𝑤))) |
20 | 4 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑤 ∈ 𝐴 ↦ (𝐹‘𝑤))) |
21 | 1, 12, 13, 19, 20 | offval2 6914 |
. . 3
⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝑤 ∈ 𝐴 ↦ ((𝐺‘𝑤)𝑅(𝐹‘𝑤)))) |
22 | 9 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝑤) = ((𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))‘𝑤)) |
23 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤)) |
24 | 23 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑁‘(𝐹‘𝑣)) = (𝑁‘(𝐹‘𝑤))) |
25 | | fvex 6201 |
. . . . . . . 8
⊢ (𝑁‘(𝐹‘𝑤)) ∈ V |
26 | 24, 7, 25 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑤 ∈ 𝐴 → ((𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))‘𝑤) = (𝑁‘(𝐹‘𝑤))) |
27 | 22, 26 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐺‘𝑤) = (𝑁‘(𝐹‘𝑤))) |
28 | 27 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐺‘𝑤)𝑅(𝐹‘𝑤)) = ((𝑁‘(𝐹‘𝑤))𝑅(𝐹‘𝑤))) |
29 | | caofinvl.6 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) |
30 | 29 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ((𝑁‘𝑥)𝑅𝑥) = 𝐵) |
31 | 30 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∀𝑥 ∈ 𝑆 ((𝑁‘𝑥)𝑅𝑥) = 𝐵) |
32 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑤) → (𝑁‘𝑥) = (𝑁‘(𝐹‘𝑤))) |
33 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑤) → 𝑥 = (𝐹‘𝑤)) |
34 | 32, 33 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑤) → ((𝑁‘𝑥)𝑅𝑥) = ((𝑁‘(𝐹‘𝑤))𝑅(𝐹‘𝑤))) |
35 | 34 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑤) → (((𝑁‘𝑥)𝑅𝑥) = 𝐵 ↔ ((𝑁‘(𝐹‘𝑤))𝑅(𝐹‘𝑤)) = 𝐵)) |
36 | 35 | rspcva 3307 |
. . . . . 6
⊢ (((𝐹‘𝑤) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ((𝑁‘𝑥)𝑅𝑥) = 𝐵) → ((𝑁‘(𝐹‘𝑤))𝑅(𝐹‘𝑤)) = 𝐵) |
37 | 13, 31, 36 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑁‘(𝐹‘𝑤))𝑅(𝐹‘𝑤)) = 𝐵) |
38 | 28, 37 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝐺‘𝑤)𝑅(𝐹‘𝑤)) = 𝐵) |
39 | 38 | mpteq2dva 4744 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ ((𝐺‘𝑤)𝑅(𝐹‘𝑤))) = (𝑤 ∈ 𝐴 ↦ 𝐵)) |
40 | 21, 39 | eqtrd 2656 |
. 2
⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝑤 ∈ 𝐴 ↦ 𝐵)) |
41 | | fconstmpt 5163 |
. 2
⊢ (𝐴 × {𝐵}) = (𝑤 ∈ 𝐴 ↦ 𝐵) |
42 | 40, 41 | syl6eqr 2674 |
1
⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝐴 × {𝐵})) |