Step | Hyp | Ref
| Expression |
1 | | df-mpt 5652 |
. . 3
⊢ (s ∈ (A ↑m G) ↦ (r ∘ s)) = {〈s, x〉 ∣ (s ∈ (A ↑m G) ∧ x = (r ∘ s))} |
2 | | enmap1lem1.1 |
. . 3
⊢ W = (s ∈ (A
↑m G) ↦ (r ∘ s)) |
3 | | opelres 4950 |
. . . . 5
⊢ (〈s, x〉 ∈ (((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↾ (A
↑m G)) ↔ (〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ∧ s ∈ (A
↑m G))) |
4 | | elima 4754 |
. . . . . . . . 9
⊢ (〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↔ ∃p ∈ Compose p(((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )〈s, x〉) |
5 | | trtxp 5781 |
. . . . . . . . . . . 12
⊢ (p(((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )〈s, x〉 ↔
(p((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st )s ∧ p2nd x)) |
6 | | brco 4883 |
. . . . . . . . . . . . . 14
⊢ (p((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st )s ↔ ∃x(p1st x ∧ x(((◡1st “ {r}) × V) ∩ 2nd )s)) |
7 | | ancom 437 |
. . . . . . . . . . . . . . . 16
⊢ ((p1st x ∧ x(((◡1st “ {r}) × V) ∩ 2nd )s) ↔ (x(((◡1st “ {r}) × V) ∩ 2nd )s ∧ p1st x)) |
8 | | brin 4693 |
. . . . . . . . . . . . . . . . . 18
⊢ (x(((◡1st “ {r}) × V) ∩ 2nd )s ↔ (x((◡1st “ {r}) × V)s
∧ x2nd s)) |
9 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ s ∈
V |
10 | | brxp 4812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (x((◡1st “ {r}) × V)s
↔ (x ∈ (◡1st “ {r}) ∧ s ∈
V)) |
11 | 9, 10 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (x((◡1st “ {r}) × V)s
↔ x ∈ (◡1st “ {r})) |
12 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (x ∈ (◡1st “ {r}) ↔ x1st r) |
13 | 11, 12 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x((◡1st “ {r}) × V)s
↔ x1st r) |
14 | 13 | anbi1i 676 |
. . . . . . . . . . . . . . . . . 18
⊢ ((x((◡1st “ {r}) × V)s
∧ x2nd s) ↔ (x1st r ∧ x2nd s)) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . . . 19
⊢ r ∈
V |
16 | 15, 9 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((x1st r ∧ x2nd s) ↔ x =
〈r,
s〉) |
17 | 8, 14, 16 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
⊢ (x(((◡1st “ {r}) × V) ∩ 2nd )s ↔ x =
〈r,
s〉) |
18 | 17 | anbi1i 676 |
. . . . . . . . . . . . . . . 16
⊢ ((x(((◡1st “ {r}) × V) ∩ 2nd )s ∧ p1st x) ↔ (x =
〈r,
s〉 ∧ p1st x)) |
19 | 7, 18 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ ((p1st x ∧ x(((◡1st “ {r}) × V) ∩ 2nd )s) ↔ (x =
〈r,
s〉 ∧ p1st x)) |
20 | 19 | exbii 1582 |
. . . . . . . . . . . . . 14
⊢ (∃x(p1st x ∧ x(((◡1st “ {r}) × V) ∩ 2nd )s) ↔ ∃x(x = 〈r, s〉 ∧ p1st x)) |
21 | 15, 9 | opex 4588 |
. . . . . . . . . . . . . . 15
⊢ 〈r, s〉 ∈ V |
22 | | breq2 4643 |
. . . . . . . . . . . . . . 15
⊢ (x = 〈r, s〉 → (p1st x ↔ p1st 〈r, s〉)) |
23 | 21, 22 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
⊢ (∃x(x = 〈r, s〉 ∧ p1st x) ↔ p1st 〈r, s〉) |
24 | 6, 20, 23 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (p((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st )s ↔ p1st 〈r, s〉) |
25 | 24 | anbi1i 676 |
. . . . . . . . . . . 12
⊢ ((p((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st )s ∧ p2nd x) ↔ (p1st 〈r, s〉 ∧ p2nd x)) |
26 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ x ∈
V |
27 | 21, 26 | op1st2nd 5790 |
. . . . . . . . . . . 12
⊢ ((p1st 〈r, s〉 ∧ p2nd x) ↔ p =
〈〈r, s〉, x〉) |
28 | 5, 25, 27 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (p(((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )〈s, x〉 ↔ p = 〈〈r, s〉, x〉) |
29 | 28 | rexbii 2639 |
. . . . . . . . . 10
⊢ (∃p ∈ Compose p(((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )〈s, x〉 ↔ ∃p ∈ Compose p = 〈〈r, s〉, x〉) |
30 | | risset 2661 |
. . . . . . . . . 10
⊢ (〈〈r, s〉, x〉 ∈ Compose ↔ ∃p ∈ Compose p = 〈〈r, s〉, x〉) |
31 | 29, 30 | bitr4i 243 |
. . . . . . . . 9
⊢ (∃p ∈ Compose p(((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )〈s, x〉 ↔ 〈〈r, s〉, x〉 ∈ Compose ) |
32 | 4, 31 | bitri 240 |
. . . . . . . 8
⊢ (〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↔ 〈〈r, s〉, x〉 ∈ Compose ) |
33 | | df-br 4640 |
. . . . . . . 8
⊢ (〈r, s〉 Compose x ↔
〈〈r, s〉, x〉 ∈ Compose ) |
34 | 32, 33 | bitr4i 243 |
. . . . . . 7
⊢ (〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↔ 〈r, s〉 Compose x) |
35 | | brcomposeg 5819 |
. . . . . . . 8
⊢ ((r ∈ V ∧ s ∈ V) → (〈r, s〉 Compose x ↔
(r ∘
s) = x)) |
36 | 15, 9, 35 | mp2an 653 |
. . . . . . 7
⊢ (〈r, s〉 Compose x ↔
(r ∘
s) = x) |
37 | | eqcom 2355 |
. . . . . . 7
⊢ ((r ∘ s) = x ↔
x = (r
∘ s)) |
38 | 34, 36, 37 | 3bitri 262 |
. . . . . 6
⊢ (〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↔ x = (r ∘ s)) |
39 | 38 | anbi2ci 677 |
. . . . 5
⊢ ((〈s, x〉 ∈ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ∧ s ∈ (A
↑m G)) ↔
(s ∈
(A ↑m G) ∧ x = (r ∘ s))) |
40 | 3, 39 | bitri 240 |
. . . 4
⊢ (〈s, x〉 ∈ (((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↾ (A
↑m G)) ↔
(s ∈
(A ↑m G) ∧ x = (r ∘ s))) |
41 | 40 | opabbi2i 4866 |
. . 3
⊢ (((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↾ (A
↑m G)) = {〈s, x〉 ∣ (s ∈ (A
↑m G) ∧ x = (r ∘ s))} |
42 | 1, 2, 41 | 3eqtr4i 2383 |
. 2
⊢ W = (((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↾ (A
↑m G)) |
43 | | 1stex 4739 |
. . . . . . . . . 10
⊢ 1st
∈ V |
44 | 43 | cnvex 5102 |
. . . . . . . . 9
⊢ ◡1st ∈ V |
45 | | snex 4111 |
. . . . . . . . 9
⊢ {r} ∈
V |
46 | 44, 45 | imaex 4747 |
. . . . . . . 8
⊢ (◡1st “ {r}) ∈
V |
47 | | vvex 4109 |
. . . . . . . 8
⊢ V ∈ V |
48 | 46, 47 | xpex 5115 |
. . . . . . 7
⊢ ((◡1st “ {r}) × V) ∈
V |
49 | | 2ndex 5112 |
. . . . . . 7
⊢ 2nd
∈ V |
50 | 48, 49 | inex 4105 |
. . . . . 6
⊢ (((◡1st “ {r}) × V) ∩ 2nd ) ∈ V |
51 | 50, 43 | coex 4750 |
. . . . 5
⊢ ((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ∈ V |
52 | 51, 49 | txpex 5785 |
. . . 4
⊢ (((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd ) ∈ V |
53 | | composeex 5820 |
. . . 4
⊢ Compose ∈
V |
54 | 52, 53 | imaex 4747 |
. . 3
⊢ ((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ∈ V |
55 | | ovex 5551 |
. . 3
⊢ (A ↑m G) ∈
V |
56 | 54, 55 | resex 5117 |
. 2
⊢ (((((((◡1st “ {r}) × V) ∩ 2nd ) ∘ 1st ) ⊗ 2nd )
“ Compose ) ↾ (A
↑m G)) ∈ V |
57 | 42, 56 | eqeltri 2423 |
1
⊢ W ∈
V |