Step | Hyp | Ref
| Expression |
1 | | fthfunc 17169 |
. . 3
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) |
2 | 1 | ssbri 5075 |
. 2
⊢ (𝐹(𝐶 Faith 𝐷)𝐺 → 𝐹(𝐶 Func 𝐷)𝐺) |
3 | | df-br 5031 |
. . . . . . 7
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
4 | | funcrcl 17125 |
. . . . . . 7
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
5 | 3, 4 | sylbi 220 |
. . . . . 6
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
6 | | oveq12 7144 |
. . . . . . . . . 10
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷)) |
7 | 6 | breqd 5041 |
. . . . . . . . 9
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝑓(𝑐 Func 𝑑)𝑔 ↔ 𝑓(𝐶 Func 𝐷)𝑔)) |
8 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 𝑐 = 𝐶) |
9 | 8 | fveq2d 6649 |
. . . . . . . . . . 11
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶)) |
10 | | isfth.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐶) |
11 | 9, 10 | eqtr4di 2851 |
. . . . . . . . . 10
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (Base‘𝑐) = 𝐵) |
12 | 11 | raleqdv 3364 |
. . . . . . . . . 10
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))) |
13 | 11, 12 | raleqbidv 3354 |
. . . . . . . . 9
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))) |
14 | 7, 13 | anbi12d 633 |
. . . . . . . 8
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦)) ↔ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)))) |
15 | 14 | opabbidv 5096 |
. . . . . . 7
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))} = {〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}) |
16 | | df-fth 17167 |
. . . . . . 7
⊢ Faith =
(𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun ◡(𝑥𝑔𝑦))}) |
17 | | ovex 7168 |
. . . . . . . 8
⊢ (𝐶 Func 𝐷) ∈ V |
18 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)) → 𝑓(𝐶 Func 𝐷)𝑔) |
19 | 18 | ssopab2i 5402 |
. . . . . . . . 9
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ⊆ {〈𝑓, 𝑔〉 ∣ 𝑓(𝐶 Func 𝐷)𝑔} |
20 | | opabss 5094 |
. . . . . . . . 9
⊢
{〈𝑓, 𝑔〉 ∣ 𝑓(𝐶 Func 𝐷)𝑔} ⊆ (𝐶 Func 𝐷) |
21 | 19, 20 | sstri 3924 |
. . . . . . . 8
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ⊆ (𝐶 Func 𝐷) |
22 | 17, 21 | ssexi 5190 |
. . . . . . 7
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} ∈ V |
23 | 15, 16, 22 | ovmpoa 7284 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Faith 𝐷) = {〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}) |
24 | 5, 23 | syl 17 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 Faith 𝐷) = {〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}) |
25 | 24 | breqd 5041 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺)) |
26 | | relfunc 17124 |
. . . . . 6
⊢ Rel
(𝐶 Func 𝐷) |
27 | 26 | brrelex12i 5571 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
28 | | breq12 5035 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓(𝐶 Func 𝐷)𝑔 ↔ 𝐹(𝐶 Func 𝐷)𝐺)) |
29 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
30 | 29 | oveqd 7152 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦)) |
31 | 30 | cnveqd 5710 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ◡(𝑥𝑔𝑦) = ◡(𝑥𝐺𝑦)) |
32 | 31 | funeqd 6346 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (Fun ◡(𝑥𝑔𝑦) ↔ Fun ◡(𝑥𝐺𝑦))) |
33 | 32 | 2ralbidv 3164 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) |
34 | 28, 33 | anbi12d 633 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦)) ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))) |
35 | | eqid 2798 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} = {〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))} |
36 | 34, 35 | brabga 5386 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))) |
37 | 27, 36 | syl 17 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹{〈𝑓, 𝑔〉 ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))) |
38 | 25, 37 | bitrd 282 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦)))) |
39 | 38 | bianabs 545 |
. 2
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) |
40 | 2, 39 | biadanii 821 |
1
⊢ (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 Fun ◡(𝑥𝐺𝑦))) |