Definition df-mfrel

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

	Ref	Expression
Assertion	df-mfrel	⊢ mFRel = ( 𝑡 ∈ V ↦ { 𝑟 ∈ 𝒫 ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) ) ∣ ( ◡ 𝑟 = 𝑟 ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmfr	⊢ mFRel
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		cmuv	⊢ mUV
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mUV ‘ 𝑡 )
7	6 6	cxp	⊢ ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) )
8	7	cpw	⊢ 𝒫 ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) )
9	3	cv	⊢ 𝑟
10	9	ccnv	⊢ ◡ 𝑟
11	10 9	wceq	⊢ ◡ 𝑟 = 𝑟
12		vc	⊢ 𝑐
13		cmvt	⊢ mVT
14	5 13	cfv	⊢ ( mVT ‘ 𝑡 )
15		vw	⊢ 𝑤
16	6	cpw	⊢ 𝒫 ( mUV ‘ 𝑡 )
17		cfn	⊢ Fin
18	16 17	cin	⊢ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin )
19		vv	⊢ 𝑣
20	12	cv	⊢ 𝑐
21	20	csn	⊢ { 𝑐 }
22	6 21	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } )
23	15	cv	⊢ 𝑤
24	19	cv	⊢ 𝑣
25	24	csn	⊢ { 𝑣 }
26	9 25	cima	⊢ ( 𝑟 “ { 𝑣 } )
27	23 26	wss	⊢ 𝑤 ⊆ ( 𝑟 “ { 𝑣 } )
28	27 19 22	wrex	⊢ ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } )
29	28 15 18	wral	⊢ ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } )
30	29 12 14	wral	⊢ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } )
31	11 30	wa	⊢ ( ◡ 𝑟 = 𝑟 ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } ) )
32	31 3 8	crab	⊢ { 𝑟 ∈ 𝒫 ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) ) ∣ ( ◡ 𝑟 = 𝑟 ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } ) ) }
33	1 2 32	cmpt	⊢ ( 𝑡 ∈ V ↦ { 𝑟 ∈ 𝒫 ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) ) ∣ ( ◡ 𝑟 = 𝑟 ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } ) ) } )
34	0 33	wceq	⊢ mFRel = ( 𝑡 ∈ V ↦ { 𝑟 ∈ 𝒫 ( ( mUV ‘ 𝑡 ) × ( mUV ‘ 𝑡 ) ) ∣ ( ◡ 𝑟 = 𝑟 ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ∀ 𝑤 ∈ ( 𝒫 ( mUV ‘ 𝑡 ) ∩ Fin ) ∃ 𝑣 ∈ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) 𝑤 ⊆ ( 𝑟 “ { 𝑣 } ) ) } )