Step | Hyp | Ref
| Expression |
1 | | coass 5571 |
. . . . 5
⊢ ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = (𝐴 ∘ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
2 | | df1o2 7459 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
3 | | pf1ind.cb |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
4 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
5 | 3, 4 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
6 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
7 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) = (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) |
8 | 2, 5, 6, 7 | mapsncnv 7790 |
. . . . . . . 8
⊢ ◡(𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) = (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})) |
9 | 8 | coeq2i 5204 |
. . . . . . 7
⊢ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ ◡(𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) = ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) |
10 | 2, 5, 6, 7 | mapsnf1o2 7791 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)):(𝐵 ↑𝑚
1𝑜)–1-1-onto→𝐵 |
11 | | f1ococnv2 6076 |
. . . . . . . 8
⊢ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)):(𝐵 ↑𝑚
1𝑜)–1-1-onto→𝐵 → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ ◡(𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) = ( I ↾ 𝐵)) |
12 | 10, 11 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ ◡(𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) = ( I ↾ 𝐵)) |
13 | 9, 12 | syl5eqr 2658 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ( I ↾ 𝐵)) |
14 | 13 | coeq2d 5206 |
. . . . 5
⊢ (𝜑 → (𝐴 ∘ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) = (𝐴 ∘ ( I ↾ 𝐵))) |
15 | 1, 14 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = (𝐴 ∘ ( I ↾ 𝐵))) |
16 | | pf1ind.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑄) |
17 | | pf1ind.cq |
. . . . . 6
⊢ 𝑄 = ran
(eval1‘𝑅) |
18 | 17, 3 | pf1f 19535 |
. . . . 5
⊢ (𝐴 ∈ 𝑄 → 𝐴:𝐵⟶𝐵) |
19 | | fcoi1 5991 |
. . . . 5
⊢ (𝐴:𝐵⟶𝐵 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴) |
20 | 16, 18, 19 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴) |
21 | 15, 20 | eqtrd 2644 |
. . 3
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = 𝐴) |
22 | | pf1ind.cp |
. . . 4
⊢ + =
(+g‘𝑅) |
23 | | pf1ind.ct |
. . . 4
⊢ · =
(.r‘𝑅) |
24 | | eqid 2610 |
. . . . . 6
⊢
(1𝑜 eval 𝑅) = (1𝑜 eval 𝑅) |
25 | 24, 3 | evlval 19345 |
. . . . 5
⊢
(1𝑜 eval 𝑅) = ((1𝑜 evalSub 𝑅)‘𝐵) |
26 | 25 | rneqi 5273 |
. . . 4
⊢ ran
(1𝑜 eval 𝑅) = ran ((1𝑜 evalSub
𝑅)‘𝐵) |
27 | | an4 861 |
. . . . . 6
⊢ (((𝑎 ∈ ran
(1𝑜 eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) ↔ ((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}))) |
28 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ran
(1𝑜 eval 𝑅) = ran (1𝑜 eval 𝑅) |
29 | 17, 3, 28 | mpfpf1 19536 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ran
(1𝑜 eval 𝑅) → (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄) |
30 | 17, 3, 28 | mpfpf1 19536 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ran
(1𝑜 eval 𝑅) → (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄) |
31 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
32 | | pf1ind.wc |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) |
33 | 31, 32 | elab 3319 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ 𝜏) |
34 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
35 | 33, 34 | syl5bbr 273 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝜏 ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
36 | 35 | anbi1d 737 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((𝜏 ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂))) |
37 | 36 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((𝜏 ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑))) |
38 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘𝑓
+ 𝑔) ∈ V |
39 | | pf1ind.we |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁)) |
40 | 38, 39 | elab 3319 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘𝑓
+ 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜁) |
41 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝑓 ∘𝑓
+ 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔)) |
42 | 41 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((𝑓 ∘𝑓
+ 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓})) |
43 | 40, 42 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝜁 ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓})) |
44 | 37, 43 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜁) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓}))) |
45 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑔 ∈ V |
46 | | pf1ind.wd |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) |
47 | 45, 46 | elab 3319 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ 𝜂) |
48 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
49 | 47, 48 | syl5bbr 273 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝜂 ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
50 | 49 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}))) |
51 | 50 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑))) |
52 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))))) |
53 | 52 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
54 | 51, 53 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓}) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
55 | | pf1ind.ad |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) |
56 | 55 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) → (𝜑 → 𝜁)) |
57 | 56 | an4s 865 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) ∧ (𝜏 ∧ 𝜂)) → (𝜑 → 𝜁)) |
58 | 57 | expimpd 627 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) → (((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜁)) |
59 | 44, 54, 58 | vtocl2ga 3247 |
. . . . . . . . . . 11
⊢ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
60 | 29, 30, 59 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ran
(1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
61 | 60 | expcomd 453 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ran
(1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
62 | 61 | impcom 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
63 | 26, 3 | mpff 19354 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ran
(1𝑜 eval 𝑅) → 𝑎:(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
64 | 63 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → 𝑎:(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
65 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑎:(𝐵 ↑𝑚
1𝑜)⟶𝐵 → 𝑎 Fn (𝐵 ↑𝑚
1𝑜)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → 𝑎 Fn (𝐵 ↑𝑚
1𝑜)) |
67 | 26, 3 | mpff 19354 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ran
(1𝑜 eval 𝑅) → 𝑏:(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
68 | 67 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → 𝑏:(𝐵 ↑𝑚
1𝑜)⟶𝐵) |
69 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑏:(𝐵 ↑𝑚
1𝑜)⟶𝐵 → 𝑏 Fn (𝐵 ↑𝑚
1𝑜)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → 𝑏 Fn (𝐵 ↑𝑚
1𝑜)) |
71 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})) = (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})) |
72 | 2, 5, 6, 71 | mapsnf1o3 7792 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})):𝐵–1-1-onto→(𝐵 ↑𝑚
1𝑜) |
73 | | f1of 6050 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})):𝐵–1-1-onto→(𝐵 ↑𝑚
1𝑜) → (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})):𝐵⟶(𝐵 ↑𝑚
1𝑜)) |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})):𝐵⟶(𝐵 ↑𝑚
1𝑜)) |
75 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝐵 ↑𝑚
1𝑜) ∈ V |
76 | 75 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (𝐵 ↑𝑚
1𝑜) ∈ V) |
77 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → 𝐵 ∈ V) |
78 | | inidm 3784 |
. . . . . . . . . 10
⊢ ((𝐵 ↑𝑚
1𝑜) ∩ (𝐵 ↑𝑚
1𝑜)) = (𝐵 ↑𝑚
1𝑜) |
79 | 66, 70, 74, 76, 76, 77, 78 | ofco 6815 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))))) |
80 | 79 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 + (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
81 | 62, 80 | sylibrd 248 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
82 | 81 | expimpd 627 |
. . . . . 6
⊢ (𝜑 → (((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
83 | 27, 82 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
84 | 83 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}))) → ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
85 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘𝑓
·
𝑔) ∈
V |
86 | | pf1ind.wf |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎)) |
87 | 85, 86 | elab 3319 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘𝑓
·
𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜎) |
88 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝑓 ∘𝑓
·
𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔)) |
89 | 88 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((𝑓 ∘𝑓
·
𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓})) |
90 | 87, 89 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (𝜎 ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓})) |
91 | 37, 90 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜎) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓}))) |
92 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))))) |
93 | 92 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
94 | 51, 93 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) → (((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓}) ↔ ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
95 | | pf1ind.mu |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) |
96 | 95 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) → (𝜑 → 𝜎)) |
97 | 96 | an4s 865 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) ∧ (𝜏 ∧ 𝜂)) → (𝜑 → 𝜎)) |
98 | 97 | expimpd 627 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄) → (((𝜏 ∧ 𝜂) ∧ 𝜑) → 𝜎)) |
99 | 91, 94, 98 | vtocl2ga 3247 |
. . . . . . . . . . 11
⊢ (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
100 | 29, 30, 99 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ran
(1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) → ((((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
101 | 100 | expcomd 453 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ran
(1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓}))) |
102 | 101 | impcom 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
103 | 66, 70, 74, 76, 76, 77, 78 | ofco 6815 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))))) |
104 | 103 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))
∘𝑓 · (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) ∈ {𝑥 ∣ 𝜓})) |
105 | 102, 104 | sylibrd 248 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅))) → (((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) → ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
106 | 105 | expimpd 627 |
. . . . . 6
⊢ (𝜑 → (((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ 𝑏 ∈ ran (1𝑜 eval 𝑅)) ∧ ((𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
107 | 27, 106 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) → ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
108 | 107 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ ((𝑎 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) ∧ (𝑏 ∈ ran (1𝑜 eval 𝑅) ∧ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}))) → ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
109 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = ((𝐵 ↑𝑚
1𝑜) × {𝑎}) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = (((𝐵 ↑𝑚
1𝑜) × {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
110 | 109 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = ((𝐵 ↑𝑚
1𝑜) × {𝑎}) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (((𝐵 ↑𝑚
1𝑜) × {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
111 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
112 | 111 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
113 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = 𝑎 → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
114 | 113 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = 𝑎 → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (𝑎 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
115 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = 𝑏 → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
116 | 115 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = 𝑏 → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ (𝑏 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
117 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = (𝑎 ∘𝑓 + 𝑏) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑎 ∘𝑓
+ 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
118 | 117 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = (𝑎 ∘𝑓 + 𝑏) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘𝑓 + 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
119 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = (𝑎 ∘𝑓 · 𝑏) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑎 ∘𝑓
·
𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
120 | 119 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = (𝑎 ∘𝑓 · 𝑏) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑎 ∘𝑓 · 𝑏) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
121 | | coeq1 5201 |
. . . . 5
⊢ (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) → (𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
122 | 121 | eleq1d 2672 |
. . . 4
⊢ (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) → ((𝑦 ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
123 | 17 | pf1rcl 19534 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑄 → 𝑅 ∈ CRing) |
124 | 16, 123 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
125 | 124 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑅 ∈ CRing) |
126 | | 1on 7454 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ On |
127 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
128 | 127 | mplassa 19275 |
. . . . . . . . . . . 12
⊢
((1𝑜 ∈ On ∧ 𝑅 ∈ CRing) → (1𝑜
mPoly 𝑅) ∈
AssAlg) |
129 | 126, 124,
128 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (1𝑜
mPoly 𝑅) ∈
AssAlg) |
130 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
131 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
132 | 130, 131 | ply1ascl 19449 |
. . . . . . . . . . . 12
⊢
(algSc‘(Poly1‘𝑅)) = (algSc‘(1𝑜
mPoly 𝑅)) |
133 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘(1𝑜 mPoly 𝑅)) = (Scalar‘(1𝑜
mPoly 𝑅)) |
134 | 132, 133 | asclrhm 19163 |
. . . . . . . . . . 11
⊢
((1𝑜 mPoly 𝑅) ∈ AssAlg →
(algSc‘(Poly1‘𝑅)) ∈
((Scalar‘(1𝑜 mPoly 𝑅)) RingHom (1𝑜 mPoly
𝑅))) |
135 | 129, 134 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)) ∈
((Scalar‘(1𝑜 mPoly 𝑅)) RingHom (1𝑜 mPoly
𝑅))) |
136 | 126 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1𝑜
∈ On) |
137 | 127, 136,
124 | mplsca 19266 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Scalar‘(1𝑜
mPoly 𝑅))) |
138 | 137 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 RingHom (1𝑜 mPoly 𝑅)) =
((Scalar‘(1𝑜 mPoly 𝑅)) RingHom (1𝑜 mPoly
𝑅))) |
139 | 135, 138 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)) ∈ (𝑅 RingHom (1𝑜 mPoly 𝑅))) |
140 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘(1𝑜 mPoly 𝑅)) = (Base‘(1𝑜
mPoly 𝑅)) |
141 | 3, 140 | rhmf 18549 |
. . . . . . . . 9
⊢
((algSc‘(Poly1‘𝑅)) ∈ (𝑅 RingHom (1𝑜 mPoly 𝑅)) →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(1𝑜
mPoly 𝑅))) |
142 | 139, 141 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(algSc‘(Poly1‘𝑅)):𝐵⟶(Base‘(1𝑜
mPoly 𝑅))) |
143 | 142 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) →
((algSc‘(Poly1‘𝑅))‘𝑎) ∈ (Base‘(1𝑜
mPoly 𝑅))) |
144 | | eqid 2610 |
. . . . . . . 8
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
145 | 144, 24, 3, 127, 140 | evl1val 19514 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧
((algSc‘(Poly1‘𝑅))‘𝑎) ∈ (Base‘(1𝑜
mPoly 𝑅))) →
((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (((1𝑜 eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 × {𝑤})))) |
146 | 125, 143,
145 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (((1𝑜 eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 × {𝑤})))) |
147 | 144, 130,
3, 131 | evl1sca 19519 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (𝐵 × {𝑎})) |
148 | 124, 147 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((eval1‘𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = (𝐵 × {𝑎})) |
149 | 3 | ressid 15762 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ CRing → (𝑅 ↾s 𝐵) = 𝑅) |
150 | 125, 149 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑅 ↾s 𝐵) = 𝑅) |
151 | 150 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (1𝑜 mPoly (𝑅 ↾s 𝐵)) = (1𝑜
mPoly 𝑅)) |
152 | 151 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (algSc‘(1𝑜
mPoly (𝑅
↾s 𝐵))) =
(algSc‘(1𝑜 mPoly 𝑅))) |
153 | 152, 132 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (algSc‘(1𝑜
mPoly (𝑅
↾s 𝐵))) =
(algSc‘(Poly1‘𝑅))) |
154 | 153 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) →
((algSc‘(1𝑜 mPoly (𝑅 ↾s 𝐵)))‘𝑎) =
((algSc‘(Poly1‘𝑅))‘𝑎)) |
155 | 154 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1𝑜 eval 𝑅)‘((algSc‘(1𝑜
mPoly (𝑅
↾s 𝐵)))‘𝑎)) = ((1𝑜 eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎))) |
156 | | eqid 2610 |
. . . . . . . . 9
⊢
(1𝑜 mPoly (𝑅 ↾s 𝐵)) = (1𝑜 mPoly (𝑅 ↾s 𝐵)) |
157 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑅 ↾s 𝐵) = (𝑅 ↾s 𝐵) |
158 | | eqid 2610 |
. . . . . . . . 9
⊢
(algSc‘(1𝑜 mPoly (𝑅 ↾s 𝐵))) = (algSc‘(1𝑜
mPoly (𝑅
↾s 𝐵))) |
159 | 126 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 1𝑜 ∈
On) |
160 | | crngring 18381 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
161 | 3 | subrgid 18605 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅)) |
162 | 124, 160,
161 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) |
163 | 162 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 ∈ (SubRing‘𝑅)) |
164 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
165 | 25, 156, 157, 3, 158, 159, 125, 163, 164 | evlssca 19343 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1𝑜 eval 𝑅)‘((algSc‘(1𝑜
mPoly (𝑅
↾s 𝐵)))‘𝑎)) = ((𝐵 ↑𝑚
1𝑜) × {𝑎})) |
166 | 155, 165 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((1𝑜 eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) = ((𝐵 ↑𝑚 1𝑜)
× {𝑎})) |
167 | 166 | coeq1d 5205 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((1𝑜 eval 𝑅)‘((algSc‘(Poly1‘𝑅))‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 × {𝑤}))) = (((𝐵 ↑𝑚 1𝑜)
× {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 × {𝑤})))) |
168 | 146, 148,
167 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) = (((𝐵 ↑𝑚
1𝑜) × {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
169 | | pf1ind.co |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝜒) |
170 | | snex 4835 |
. . . . . . . . . 10
⊢ {𝑓} ∈ V |
171 | 5, 170 | xpex 6860 |
. . . . . . . . 9
⊢ (𝐵 × {𝑓}) ∈ V |
172 | | pf1ind.wa |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 × {𝑓}) → (𝜓 ↔ 𝜒)) |
173 | 171, 172 | elab 3319 |
. . . . . . . 8
⊢ ((𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ 𝜒) |
174 | 169, 173 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓}) |
175 | 174 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓}) |
176 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑓 = 𝑎 → {𝑓} = {𝑎}) |
177 | 176 | xpeq2d 5063 |
. . . . . . . 8
⊢ (𝑓 = 𝑎 → (𝐵 × {𝑓}) = (𝐵 × {𝑎})) |
178 | 177 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑓 = 𝑎 → ((𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓})) |
179 | 178 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑓 ∈
𝐵 (𝐵 × {𝑓}) ∈ {𝑥 ∣ 𝜓} ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓}) |
180 | 175, 179 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐵 × {𝑎}) ∈ {𝑥 ∣ 𝜓}) |
181 | 168, 180 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝐵 ↑𝑚
1𝑜) × {𝑎}) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
182 | | pf1ind.pr |
. . . . . . . 8
⊢ (𝜑 → 𝜃) |
183 | | resiexg 6994 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → ( I ↾
𝐵) ∈
V) |
184 | 5, 183 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ 𝐵) ∈
V |
185 | | pf1ind.wb |
. . . . . . . . 9
⊢ (𝑥 = ( I ↾ 𝐵) → (𝜓 ↔ 𝜃)) |
186 | 184, 185 | elab 3319 |
. . . . . . . 8
⊢ (( I
↾ 𝐵) ∈ {𝑥 ∣ 𝜓} ↔ 𝜃) |
187 | 182, 186 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ( I ↾ 𝐵) ∈ {𝑥 ∣ 𝜓}) |
188 | 13, 187 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
189 | | el1o 7466 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 1𝑜
↔ 𝑎 =
∅) |
190 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = ∅ → (𝑏‘𝑎) = (𝑏‘∅)) |
191 | 189, 190 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑎 ∈ 1𝑜
→ (𝑏‘𝑎) = (𝑏‘∅)) |
192 | 191 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑎 ∈ 1𝑜
→ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) = (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) |
193 | 192 | coeq1d 5205 |
. . . . . . 7
⊢ (𝑎 ∈ 1𝑜
→ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) = ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤})))) |
194 | 193 | eleq1d 2672 |
. . . . . 6
⊢ (𝑎 ∈ 1𝑜
→ (((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓} ↔ ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
195 | 188, 194 | syl5ibrcom 236 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ 1𝑜 → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓})) |
196 | 195 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 1𝑜) → ((𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘𝑎)) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
197 | 17, 3, 28 | pf1mpf 19537 |
. . . . 5
⊢ (𝐴 ∈ 𝑄 → (𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∈ ran
(1𝑜 eval 𝑅)) |
198 | 16, 197 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∈ ran
(1𝑜 eval 𝑅)) |
199 | 3, 22, 23, 26, 84, 108, 110, 112, 114, 116, 118, 120, 122, 181, 196, 198 | mpfind 19357 |
. . 3
⊢ (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵 ↑𝑚
1𝑜) ↦ (𝑏‘∅))) ∘ (𝑤 ∈ 𝐵 ↦ (1𝑜 ×
{𝑤}))) ∈ {𝑥 ∣ 𝜓}) |
200 | 21, 199 | eqeltrrd 2689 |
. 2
⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓}) |
201 | | pf1ind.wg |
. . . 4
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) |
202 | 201 | elabg 3320 |
. . 3
⊢ (𝐴 ∈ 𝑄 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
203 | 16, 202 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
204 | 200, 203 | mpbid 221 |
1
⊢ (𝜑 → 𝜌) |