Metamath Proof Explorer

Definition df-mfrel

Description: Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mfrel 
|- mFRel = ( t e. _V |-> { r e. ~P ( ( mUV ` t ) X. ( mUV ` t ) ) | ( `' r = r /\ A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfr 
 |-  mFRel
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vr 
 |-  r
4 cmuv 
 |-  mUV
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mUV ` t )
7 6 6 cxp 
 |-  ( ( mUV ` t ) X. ( mUV ` t ) )
8 7 cpw 
 |-  ~P ( ( mUV ` t ) X. ( mUV ` t ) )
9 3 cv 
 |-  r
10 9 ccnv 
 |-  `' r
11 10 9 wceq 
 |-  `' r = r
12 vc 
 |-  c
13 cmvt 
 |-  mVT
14 5 13 cfv 
 |-  ( mVT ` t )
15 vw 
 |-  w
16 6 cpw 
 |-  ~P ( mUV ` t )
17 cfn 
 |-  Fin
18 16 17 cin 
 |-  ( ~P ( mUV ` t ) i^i Fin )
19 vv 
 |-  v
20 12 cv 
 |-  c
21 20 csn 
 |-  { c }
22 6 21 cima 
 |-  ( ( mUV ` t ) " { c } )
23 15 cv 
 |-  w
24 19 cv 
 |-  v
25 24 csn 
 |-  { v }
26 9 25 cima 
 |-  ( r " { v } )
27 23 26 wss 
 |-  w C_ ( r " { v } )
28 27 19 22 wrex 
 |-  E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } )
29 28 15 18 wral 
 |-  A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } )
30 29 12 14 wral 
 |-  A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } )
31 11 30 wa 
 |-  ( `' r = r /\ A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } ) )
32 31 3 8 crab 
 |-  { r e. ~P ( ( mUV ` t ) X. ( mUV ` t ) ) | ( `' r = r /\ A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } ) ) }
33 1 2 32 cmpt 
 |-  ( t e. _V |-> { r e. ~P ( ( mUV ` t ) X. ( mUV ` t ) ) | ( `' r = r /\ A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } ) ) } )
34 0 33 wceq 
 |-  mFRel = ( t e. _V |-> { r e. ~P ( ( mUV ` t ) X. ( mUV ` t ) ) | ( `' r = r /\ A. c e. ( mVT ` t ) A. w e. ( ~P ( mUV ` t ) i^i Fin ) E. v e. ( ( mUV ` t ) " { c } ) w C_ ( r " { v } ) ) } )