Metamath Proof Explorer


Theorem ismre

Description: Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion ismre C Moore X C 𝒫 X X C s 𝒫 C s s C

Proof

Step Hyp Ref Expression
1 elfvex C Moore X X V
2 elex X C X V
3 2 3ad2ant2 C 𝒫 X X C s 𝒫 C s s C X V
4 pweq x = X 𝒫 x = 𝒫 X
5 4 pweqd x = X 𝒫 𝒫 x = 𝒫 𝒫 X
6 eleq1 x = X x c X c
7 6 anbi1d x = X x c s 𝒫 c s s c X c s 𝒫 c s s c
8 5 7 rabeqbidv x = X c 𝒫 𝒫 x | x c s 𝒫 c s s c = c 𝒫 𝒫 X | X c s 𝒫 c s s c
9 df-mre Moore = x V c 𝒫 𝒫 x | x c s 𝒫 c s s c
10 vpwex 𝒫 x V
11 10 pwex 𝒫 𝒫 x V
12 11 rabex c 𝒫 𝒫 x | x c s 𝒫 c s s c V
13 8 9 12 fvmpt3i X V Moore X = c 𝒫 𝒫 X | X c s 𝒫 c s s c
14 13 eleq2d X V C Moore X C c 𝒫 𝒫 X | X c s 𝒫 c s s c
15 eleq2 c = C X c X C
16 pweq c = C 𝒫 c = 𝒫 C
17 eleq2 c = C s c s C
18 17 imbi2d c = C s s c s s C
19 16 18 raleqbidv c = C s 𝒫 c s s c s 𝒫 C s s C
20 15 19 anbi12d c = C X c s 𝒫 c s s c X C s 𝒫 C s s C
21 20 elrab C c 𝒫 𝒫 X | X c s 𝒫 c s s c C 𝒫 𝒫 X X C s 𝒫 C s s C
22 21 a1i X V C c 𝒫 𝒫 X | X c s 𝒫 c s s c C 𝒫 𝒫 X X C s 𝒫 C s s C
23 pwexg X V 𝒫 X V
24 elpw2g 𝒫 X V C 𝒫 𝒫 X C 𝒫 X
25 23 24 syl X V C 𝒫 𝒫 X C 𝒫 X
26 25 anbi1d X V C 𝒫 𝒫 X X C s 𝒫 C s s C C 𝒫 X X C s 𝒫 C s s C
27 3anass C 𝒫 X X C s 𝒫 C s s C C 𝒫 X X C s 𝒫 C s s C
28 26 27 syl6bbr X V C 𝒫 𝒫 X X C s 𝒫 C s s C C 𝒫 X X C s 𝒫 C s s C
29 14 22 28 3bitrd X V C Moore X C 𝒫 X X C s 𝒫 C s s C
30 1 3 29 pm5.21nii C Moore X C 𝒫 X X C s 𝒫 C s s C