Definition df-mfrel 31516

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

Assertion

Ref	Expression
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 } ) ) } )

Distinct variable group:   r, c, t, v, w

Detailed syntax breakdown of Definition df-mfrel

Step	Hyp	Ref	Expression
1		cmfr 31504	. 2 class mFRel
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vr	. . . . . . . 8 setvar r
5	4	cv 1482	. . . . . . 7 class r
6	5	ccnv 5113	. . . . . 6 class `' r
7	6, 5	wceq 1483	. . . . 5 wff `' r = r
8		vw	. . . . . . . . . 10 setvar w
9	8	cv 1482	. . . . . . . . 9 class w
10		vv	. . . . . . . . . . . 12 setvar v
11	10	cv 1482	. . . . . . . . . . 11 class v
12	11	csn 4177	. . . . . . . . . 10 class { v }
13	5, 12	cima 5117	. . . . . . . . 9 class ( r " { v } )
14	9, 13	wss 3574	. . . . . . . 8 wff w C_ ( r " { v } )
15	2	cv 1482	. . . . . . . . . 10 class t
16		cmuv 31500	. . . . . . . . . 10 class mUV
17	15, 16	cfv 5888	. . . . . . . . 9 class (mUV ` t )
18		vc	. . . . . . . . . . 11 setvar c
19	18	cv 1482	. . . . . . . . . 10 class c
20	19	csn 4177	. . . . . . . . 9 class { c }
21	17, 20	cima 5117	. . . . . . . 8 class ( (mUV ` t ) " { c } )
22	14, 10, 21	wrex 2913	. . . . . . 7 wff E. v e. ( (mUV ` t ) " { c } ) w C_ ( r " { v } )
23	17	cpw 4158	. . . . . . . 8 class ~P (mUV ` t )
24		cfn 7955	. . . . . . . 8 class Fin
25	23, 24	cin 3573	. . . . . . 7 class ( ~P (mUV ` t ) i^i Fin )
26	22, 8, 25	wral 2912	. . . . . 6 wff A. w e. ( ~P (mUV ` t ) i^i Fin ) E. v e. ( (mUV ` t ) " { c } ) w C_ ( r " { v } )
27		cmvt 31360	. . . . . . 7 class mVT
28	15, 27	cfv 5888	. . . . . 6 class (mVT ` t )
29	26, 18, 28	wral 2912	. . . . 5 wff A. c e. (mVT ` t ) A. w e. ( ~P (mUV ` t ) i^i Fin ) E. v e. ( (mUV ` t ) " { c } ) w C_ ( r " { v } )
30	7, 29	wa 384	. . . 4 wff ( `' 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 } ) )
31	17, 17	cxp 5112	. . . . 5 class ( (mUV ` t ) X. (mUV ` t ) )
32	31	cpw 4158	. . . 4 class ~P ( (mUV ` t ) X. (mUV ` t ) )
33	30, 4, 32	crab 2916	. . 3 class { 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	2, 3, 33	cmpt 4729	. 2 class ( 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 } ) ) } )
35	1, 34	wceq 1483	1 wff 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 } ) ) } )

This definition is referenced by: (None)