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∈V⟼r∈𝒫mUV⁡t×mUV⁡t|r-1=r∧∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfr classmFRel
1 vt setvart
2 cvv classV
3 vr setvarr
4 cmuv classmUV
5 1 cv setvart
6 5 4 cfv classmUV⁡t
7 6 6 cxp classmUV⁡t×mUV⁡t
8 7 cpw class𝒫mUV⁡t×mUV⁡t
9 3 cv setvarr
10 9 ccnv classr-1
11 10 9 wceq wffr-1=r
12 vc setvarc
13 cmvt classmVT
14 5 13 cfv classmVT⁡t
15 vw setvarw
16 6 cpw class𝒫mUV⁡t
17 cfn classFin
18 16 17 cin class𝒫mUV⁡t∩Fin
19 vv setvarv
20 12 cv setvarc
21 20 csn classc
22 6 21 cima classmUV⁡tc
23 15 cv setvarw
24 19 cv setvarv
25 24 csn classv
26 9 25 cima classrv
27 23 26 wss wffw⊆rv
28 27 19 22 wrex wff∃v∈mUV⁡tcw⊆rv
29 28 15 18 wral wff∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv
30 29 12 14 wral wff∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv
31 11 30 wa wffr-1=r∧∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv
32 31 3 8 crab classr∈𝒫mUV⁡t×mUV⁡t|r-1=r∧∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv
33 1 2 32 cmpt classt∈V⟼r∈𝒫mUV⁡t×mUV⁡t|r-1=r∧∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv
34 0 33 wceq wffmFRel=t∈V⟼r∈𝒫mUV⁡t×mUV⁡t|r-1=r∧∀c∈mVT⁡t∀w∈𝒫mUV⁡t∩Fin∃v∈mUV⁡tcw⊆rv